[GHC] #11732: Deriving Generic1 interacts poorly with TypeInType

[GHC]

#11732: Deriving Generic1 interacts poorly with TypeInType
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:  TypeInType,
                                     |  Generics
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 goldfire):

 There is a small problem here:

 {{{
 instance (k ~ *) => Functor (P1 (a :: k))
 }}}

 doesn't type-check. The problem is that this requires "immediate" use of
 the kind equality. In other words, we would need to give a name to the
 kind equality in order to cast by it later in the same type. But, last
 spring, Simon and I decided it would be simpler not to allow binding of
 kind equalities in types -- we can now bind them only in terms. (See also
 the first bullet [wiki:DependentHaskell/Phase1#Answers here].)

 Ignoring this issue, let's consider

 1. `instance (k ~ *) => Functor (P2 k)`
 2. `instance Functor (P2 *)`

 I claim that these (if the first were to type-check) instances are
 entirely equivalent. Normally, inlining an equality constraint changes the
 meaning of an instance, but not here. The first instance matches `Functor
 (P2 k)` for any value of `k`. What's interesting is that the second
 instance, exactly as written, does too. That's because the only possible
 value for `k` in `Functor (P2 k)` is `*`. Anything else is surely ill-
 typed. Accordingly, we should be comfortable just using the second
 instance. And I believe that anytime this sort of instantiation would
 happen has this property (that anything else would be ill-typed).

 This all means we can just do nothing about this particular issue. Which
 is nice.

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