[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 RyanGlScott):

 Replying to [comment:3 goldfire]:
 > 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.

 This requires Dependent Haskell, I presume?

 > 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.

 One correction: `deriving` only uses HsSyn for derived //methods//. It
 does in fact generate `Core` for the RHS of type instances. So what you
 describe might be possible today? (I'm not sure I follow the other
 details, so it's hard for me to say.)

 > 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
 > }}}

 `axIdentity`? What sorcery is this?

 > 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.

 Interesting. Is there a program that exhibits this bug (that doesn't
 leverage this GND business)?

 > 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.

 Indeed. And we could quite easily change this design in the future, so I'm
 not too worried about being conservative for now.

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