| 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:ben@smart-cactus.org]
| Sent: 03 February 2017 16:01
| To: Simon Peyton Jones ; Richard Eisenberg
|
| Cc: ghc-devs@haskell.org
| Subject: RE: Panic from rewritableTyVarsOfType
|
| Ben Gamari writes:
|
| > Simon Peyton Jones 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
