[GHC] #14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?

[GHC]

#14728: Is (GeneralizedNewtypeDeriving + associated type classes) completely bogus?
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.2
  checker)                           |             Keywords:  deriving,
      Resolution:                    |  TypeFamilies
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):

 `type T (Identity a) x = T a x` is ill-kinded, sure enough. Let's write
 out the details:

 {{{
 Identity :: Type -> Type
 'Identity :: forall (a :: Type). a -> Identity a
 T :: pi (x :: Type) -> x -> Type

 type instance forall (a :: Type) (x :: Identity a). T (Identity a) x = T a
 x
 }}}

 In the last line, the `x` has the wrong kind: it has kind `Identity a`,
 where it really should have kind `a`. Here's the correct type instance:

 {{{
 type instance forall (a :: Type) (x :: Identity a). T (Identity a) x = T a
 ('runIdentity x)
 }}}

 where I've used `'` to use the term-level `runIdentity` function in a
 type.

 I don't think this would be impossible to support. Currently, the
 `deriving` mechanism produces HsSyn. I suppose that makes it easier w.r.t.
 inferring contexts and such. But suppose we could write the RHS of type
 instances in Core, and use `HsCoreTy` to embed it into HsSyn. Then,
 `runIdentity` is just a cast by the axiom induced by the `Identity`
 newtype.

 But it gets more complicated, sadly.

 {{{
 class D a where
   type S a (x :: Maybe a)
 deriving instance D (Identity a)
 }}}

 This would need to produce

 {{{
 type instance forall (a :: Type) (x :: Maybe (Identity a)). S (Identity a)
 x = S a (x |> g)
   where
     g :: Maybe (Identity a) ~ Maybe a
     g = Maybe axIdentity
 }}}

 This example shows us that just using the newtype axiom isn't enough. We
 need to take the type of `x`, find all occurrences of `a` in it, and
 rewrite those to be `axIdentity` instead. Happily, GHC already has
 implemented this operation: it's called `Coercion.liftCoSubst`. A detailed
 explanation of lifting is in the "System FC with Explicit Kind Equalities"
 paper (among other places, I think). It's useful when you have a coercion
 between `ty1` and `ty2` (in our case, the newtype axiom) and you need a
 coercion between `ty3[ty1/a]` and `ty3[ty2/a]` -- precisely our scenario.

 But it gets even worse.

 Suppose now later parameters to the type family depend on `x`. These will
 have to account for the change in `x`'s type. So we need a coercion
 relating the old `x` to the new, casted `x`, which will then be used to
 cast those later parameters. Happily, I've already worked out the
 algorithm to deal with this more general case, and I've implemented it in
 my branch (github.com/goldfirere/ghc, on the wip/rae branch), in
 `TcFlatten.flatten_args`. This branch is not merged due to performance
 trouble, but the algorithm is correct.

 Actually, as I'm writing this all up, I realize that
 `FamInstEnv.normaliseType` is behind the times here. It, too, needs to
 take all of these challenges into account in order to produce a well-
 kinded output. I'll post a new bug to this effect.

 Is it worth doing all of these here, for GND? Probably not. And I think
 the idea of "just don't allow this" may be best. However, it's good to
 know that we ''could'' do this if we wanted.

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