Panic from rewritableTyVarsOfType

[Ben Gamari]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170203/e53aab0c/attachment-0001.sig>