[GHC] #8503: New GeneralizedNewtypeDeriving check still isn't permissive enough

[GHC]

#8503: New GeneralizedNewtypeDeriving check still isn't permissive enough
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:  goldfire
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.7
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 Yuck.

 I'm leery of creating a way for the type-checker to loop without turning
 on `UndecidableInstances`. And, with the `R2` example that Simon gives,
 the newtype and the relevant type family instance might be in different
 modules, so detecting even so simple an infinite regress may be
 problematic. (And, note that the pieces on their own are innocent-
 looking.)

 I've also just looked at `Note [Recursive newtypes]` in !TcDeriv. This
 note explains why GND ''works'' for recursive newtypes. I repeat it here:

 {{{
 Note [Recursive newtypes]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Newtype deriving works fine, even if the newtype is recursive.
 e.g.    newtype S1 = S1 [T1 ()]
         newtype T1 a = T1 (StateT S1 IO a ) deriving( Monad )
 Remember, too, that type families are curretly (conservatively) given
 a recursive flag, so this also allows newtype deriving to work
 for type famillies.

 We used to exclude recursive types, because we had a rather simple
 minded way of generating the instance decl:
    newtype A = MkA [A]
    instance Eq [A] => Eq A      -- Makes typechecker loop!
 But now we require a simple context, so it's ok.
 }}}

 I'm confused by the last line. In the code above the note, a context is
 generated that includes, for this example, `Eq [A]`! Where does the loop
 get broken?

 Regardless, here's a possible solution: if `Coercible` over recursive
 newtypes is sound but otherwise in danger of causing a loop, we could just
 require `UndecidableInstances` to get the `Coercible` mechanism to go down
 this road. In this scenario, my example (with `RecNT`) would fail to use
 GND without `UndecidableInstances` but should succeed with it. We can even
 give a helpful error message in this scenario.

 Or, perhaps even better: could the `Coercible` mechanism use
 `TyCon.checkRecTc`? That function seems to be designed for exactly this
 scenario, which is where we need to do newtype expansion but don't want to
 fall into a black hole. That might complicate the `Coercible` code, but I
 think it would be a step in the right direction. We could still allow
 users to specify `UndecidableInstances` to bypass even this check... but
 my guess is that `checkRecTc` would work exactly in the correct cases,
 meaning that bypassing the check is sure to cause the type-checker to
 loop. Other, more informed opinions are very welcome here.

 Lastly, is there a solid reason to require that the recursiveness of a
 type in a hs-boot file and the recursiveness of the real type are the
 same? It looks to me that it would be sound to assume types in hs-boot
 files are recursive, but then not to inherit this trait when processing
 the real thing. That would fix the problem with compiling Module.lhs, and
 it would save some embarrassment if we were to suggest
 `UndecidableInstances` to compile a very ordinary-looking newtype!

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