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

27 Jan 2018

      #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):

 I can see two ways out of this mess:

 1. We should kind-check associated type family instances that are
 generated in derived code. This would have caught these mistakes early
 (and just seems like a good idea in general). Currently, we simply
 generate `Type`s directly in `TcGenDeriv`, so we have to take it on faith
 that `TcGenDeriv` is doing the right thing.
 2. Disallow occurrences of the derived class's last type parameter as a
 //kind// within an associated type family. I believe the sketchiness
 witnesses above only happens when this criterion is met, so we could just
 disallow that wholesale.

    One downside is that there would actually be a small class of programs
 that would be ruled out by this restriction. Namely:

 {{{#!hs
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind

 class C (a :: Type) where
   type T a (x :: a) :: Type

 newtype Loop = Loop Loop

 deriving instance C Loop
 }}}

    This currently compiles (and genuinely kind-checks), but would fail to
 compile if we instituted the aforementioned kind validity check. But this
 isn't too much of a loss, as actually trying to use the `T` instance for
 `Loop` would, well, infinitely loop. :)

 Option (2) sounds much simpler, so I think I'd be inclined to favor that
 for the time being.

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