Panic from rewritableTyVarsOfType

[Simon Peyton Jones]

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