[GHC] #14147: Confusing error messages with PolyKinds and superclasses

[GHC]

#14147: Confusing error messages with PolyKinds and superclasses
-------------------------------------+-------------------------------------
        Reporter:  enolan            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 So here is what's going on. Nowadays, every datatype automatically has a
 `Typeable` instance emitted (so `deriving Typeable` is redundant). A
 datatype is `Typeable` only if all of its type parameters are also
 `Typeable`. So //without// `PolyKinds` enabled, the emitted `Typeable`
 instance for `Tagged` is:

 {{{#!hs
 instance (Typeable t, Typeable v) => Typeable (Tagged t v)
 }}}

 So far, so good. Now what happens when you turn on `PolyKinds`? By
 default, `PolyKinds` generalizes the kind of every type variable to the
 fullest extent it can. Notice that in the definition of `Tagged`:

 {{{#!hs
 newtype Tagged t v = Tagged v
 }}}

 Here, `v` is used as a field, so its kind must be `*`. But `t` is
 completely unconstrained, so its kind is generalized to `k`, a kind
 variable.

 Now, you claimed that "don't have a `k` variable anywhere". But that's not
 true—`Tagged` //does// have a `k` parameter, except that it's invisible
 (as opposed to `t` and `v`, which are visible). If you enable `-fprint-
 explicit-foralls`, it's much easier to see this in action:

 {{{
 λ> :set -XPolyKinds
 λ> newtype Tagged t v = Tagged v
 λ> :set -fprint-explicit-foralls
 λ> :type +v Tagged
 Tagged :: forall {k} (t :: k) v. v -> Tagged t v
 }}}

 With this in mind, let's revisit the `Typeable` instance for `Tagged`.
 Recall that a datatype is `Typeable` only if all of its type parameters
 are also `Typeable`. Therefore, with `PolyKinds` enabled, the emitted
 `Typeable` instance is:

 {{{#!hs
 instance (Typeable k, Typeable t, Typeable v) => Typeable (Tagged (t :: k)
 v)
 }}}

 Hopefully now it will become clear why you experienced that `Could not
 deduce (Typeable k)` error message: you had written this instance:

 {{{#!hs
 instance Typeable t => MyClass (Tagged t Int)
 }}}

 Because `Typeable` is a superclass of `MyClass`, there needs to be a
 `Typeable (Tagged (t :: k) Int)` instance in scope for this to typecheck.
 But the only constraint on this instance is `Typeable t`—we don't know
 that `k` is also `Typeable`! Therefore, fixing this is a matter of adding
 an extra constraint:

 {{{#!hs
 instance (Typeable k, Typeable t) => MyClass (Tagged (t :: k) Int)
 }}}

 (This requires the `TypeInType` language extension, which is essentially a
 beefed up version of `PolyKinds`.)

 So to recap, I'd argue that there's no bug here, just a tricky interaction
 between the `Typeable` solver and language extensions. Enabling
 `PolyKinds` (and thus generalizing kinds) is certainly not guaranteed to
 keep your existing code compiling!

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14147#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler