[GHC] #9371: Overlapping type families, segafult

[GHC]

#9371: Overlapping type families, segafult
----------------------------------------+----------------------------------
              Reporter:  pingu          |            Owner:
                  Type:  bug            |           Status:  new
              Priority:  normal         |        Milestone:
             Component:  Compiler       |          Version:  7.8.3
            Resolution:                 |         Keywords:
      Operating System:  Linux          |     Architecture:  x86_64 (amd64)
       Type of failure:  Runtime crash  |       Difficulty:  Unknown
             Test Case:                 |       Blocked By:
              Blocking:                 |  Related Tickets:
Differential Revisions:                 |
----------------------------------------+----------------------------------
Changes (by simonpj):

 * cc: goldfire, dimitris@…, sweirich@…, nomeata, Conor.McBride@… (added)


Comment:

 Great bug!  I know exactly what is going on.

 There is a long-standing awkwardness in GHC’s implementation of newtype,
 described in `Note [Newtype eta]` in `TyCon`, which I reproduce below.
 The core of it comes down to this.  Consider
 {{{
 newtype Parser a = MkParser (IO a) derriving( Monad )
 }}}
 Do we have `(Monad Parser ~R Monad IO)`?  These are the types of the Monad
 dictionaries for Parser and IO resp.  In the olden days to implement
 Generalised Newtype Deriving (GND) we coerced directly between these
 dictionary types, so we really needed them to be ~R.  As a result, the
 axiom induced by the above newtype had to be
 {{{
         ax :: Parser ~R IO
 }}}
 and not
 {{{
         ax a :: Parser a  ~R  IO a
 }}}
 So we had to eta-reduce axioms.

 This is a royal pain.  And we have to do it for newtype instances too.
 See `Note [Eta reduction for data family axioms]` in `TcInstDcls`. And it
 turns out that the new, serious bug #9371 is directly attributable to this
 royal pain.

 Side note: our [http://research.microsoft.com/en-
 us/um/people/simonpj/papers/ext-f/ Safe coercions” paper] does not say in
 Section 2 how to deal with data/newtype instances.

 NOW, in our new story for GND, we never coerce between `Monad Parser` and
 `Monad IO`.  Instead we coerce the individual methods (Section 7 of the
 paper).  Why?   I think it’s because our roles are not higher-kinded, but
 we didn’t document the change. Does anyone else remember?  I think there
 were actually multiple reasons.

 However this change means that we DON’T need `(IO ~R Parser)` any more!
 Only `(IO ty  ~R  Parser ty)`.  So the reason for the eta reduction seems
 to have gone away.

 Do you agree?  If  so I could simplify GHC by removing the complicated eta
 stuff.  I would rather do that than fix #9371 by adding more complexity

 I see that this was actually proposed in #8503, but the thread diverged
 onto other matters.  Richard’s last comment:7 said “So we don't need eta-
 reduction as much as maybe we once did, but it's still useful.” but
 provided no evidence in support of this claim.

 I somehow think this is connected to #9123 but I can’t put my finger on
 why.

 Simon

 {{{
 Note [Newtype eta]
 ~~~~~~~~~~~~~~~~~~
 Consider
         newtype Parser a = MkParser (IO a) derriving( Monad )
 Are these two types equal (to Core)?
         Monad Parser
         Monad IO
 which we need to make the derived instance for Monad Parser.

 Well, yes.  But to see that easily we eta-reduce the RHS type of
 Parser, in this case to ([], Froogle), so that even unsaturated
 applications
 of Parser will work right.  This eta reduction is done when the type
 constructor is built, and cached in NewTyCon.  The cached field is
 only used in coreExpandTyCon_maybe.

 Here's an example that I think showed up in practice
 Source code:
         newtype T a = MkT [a]
         newtype Foo m = MkFoo (forall a. m a -> Int)

         w1 :: Foo []
         w1 = ...

         w2 :: Foo T
         w2 = MkFoo (\(MkT x) -> case w1 of MkFoo f -> f x)

 After desugaring, and discarding the data constructors for the newtypes,
 we get:
         w2 :: Foo T
         w2 = w1
 And now Lint complains unless Foo T == Foo [], and that requires T==[]

 This point carries over to the newtype coercion, because we need to
 say
         w2 = w1 `cast` Foo CoT

 so the coercion tycon CoT must have
         kind:    T ~ []
  and    arity:   0
 }}}

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