| Typeable1.hs:22:5: error: | • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’ | with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
I still don't see why we end up equating a polykind with a kind. | Anyways, hopefully this will be resolved with the fix to Simon's second | issue. Otherwise I just need to look at two performance regressions and I | think I'm done. I'm validating a patch that uses tyCoVarsOfType, but a bit more selectively. So you'll get the same error. S | -----Original Message----- | From: Ben Gamari [mailto:b...@smart-cactus.org] | Sent: 03 February 2017 16:01 | To: Simon Peyton Jones <simo...@microsoft.com>; Richard Eisenberg | <r...@cs.brynmawr.edu> | Cc: ghc-devs@haskell.org | Subject: RE: Panic from rewritableTyVarsOfType | | Ben Gamari <b...@smart-cactus.org> writes: | | > Simon Peyton Jones <simo...@microsoft.com> writes: | > | >> Meanwhile to get you rolling, you can replace rewritableTyVars with | >> tyCoVarsOfType and it'll all work, just a bit less efficiently. | >> | > Thanks Simon! Indeed that allows things to proceed and in the process, | > confirms that there is a bug in my solver logic. | > | I should clarify: the bug is in fact not in the Typeable solver. The problem | is that we have a type with some kind polymorphism. For instance, | | data Proxy (a :: k) = Proxy | | Note that in order to be `Typeable` Proxy needs to have its `k` kind | argument instantiated. Consequently this program is perfectly fine, | | ty :: TypeRep (Proxy Int) | ty = typeRep | | We can even decompose this into a type application, | | case ty of | TRApp a b -> ... | | where `a :: TypeRep Proxy` (with `k ~ Type`) and `b :: TypeRep Int`. | However, if we attempt to decompose `a` again (which is what the | Typeable1 testcase described in this thread tests), we run into trouble, | | case a of | TRApp x y -> ... | | After changing rewritableTyVars with tyCoVarsOfType, the testcase | Typeable1 fails with the following correct, albeit not terribly readable, | error message, | | Typeable1.hs:22:5: error: | • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’ | with ‘forall k. (* -> *) -> (k -> *) -> k -> *’ | Inaccessible code in | a pattern with pattern synonym: | TRApp :: forall k2 (t :: k2). | () => | forall k1 (a :: k1 -> k2) (b :: k1). | t ~ a b => | TypeRep (k1 -> k2) a -> TypeRep k1 b -> TypeRep k2 t, | in a pattern binding in | 'do' block | • In the pattern: TRApp x y | In a stmt of a 'do' block: TRApp x y <- pure x | In the expression: | do let x :: ComposeK Maybe Maybe Int | x = undefined | TRApp x y <- pure $ typeOf x | print (x, y) | TRApp x y <- pure x | .... | • Relevant bindings include | y :: TypeRep k3 b2 (bound at Typeable1.hs:19:13) | x :: TypeRep (k3 -> k2 -> k1 -> *) a2 (bound at | Typeable1.hs:19:11) | | This might be a place where GHC could hold the user's hand a bit more | gently. | | Anyways, hopefully this will be resolved with the fix to Simon's second | issue. Otherwise I just need to look at two performance regressions and I | think I'm done. | | Cheers, | | - Ben _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
