[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:                 |
----------------------------------------+----------------------------------

Comment (by goldfire):

 At first reading, it seemed that comment:3 did not relate to this ticket.
 But, looking closer, I see how. I'll explain for others' benefit:

 The line `data D x = D1 (Either x ())` becomes somewhat like the two
 declarations

 {{{
 data DFInst1 x = D1 (Either x ())
 type D x = DFInst1 x
 }}}

 We create a proper datatype `DFInst1` that has no eta-reduction or
 anything strange, really, other than the fact that the user can't ever
 write its name. Data families are internally interpreted somewhat like
 type families, and thus we create the connection between `D` and
 `DFInst1`. However, as Simon explains, the ''second'' of my definitions
 above is eta-reduced.

 When processing `data D (x, y) = D2 (x, y)`, the relevant type-ish
 instance is `D (x, y) = DFInst2 x y`, which can''not'' be eta-reduced.
 Then, when comparing the instances `D = DFInst1` and `D (x, y) = DFInst2 x
 y`, the conflict-checker says that the left-hand sides (`<empty>` and
 `(x,y)`, respectively) are quite surely apart, because they are of
 different lengths!

 There is a fix here that involves much less theory than Simon's approach:
 fix the conflict checker to take this into account. There should ''never''
 be different lengths involved here (absent the eta-reduction), so when
 there are, we could just note a conflict. Even simpler, we could notice
 somehow that a data family is involved and spit out a conflict right away,
 as two data family instances are ''never'' compatible.

 That said, Simon asks a worthwhile question: do we need eta-reduction
 given the new implementation of GND? I think "yes":

 {{{
 import Control.Monad.Trans.Identity

 newtype MyList a = MkList [a]
 class C m where
   x :: IdentityT m Int
 instance C [] where
   x = IdentityT [1,2,3]
 deriving instance C MyList
 }}}

 This (silly) example requires the eta-reduction to work, and I don't see a
 compelling reason to reduce expressivity here. Yes, it would simplify the
 code somewhat, but I still don't think it's worth it.

 In answer to Simon's "why not cast `Monad Parser` to `Monad IO`": a lack
 of higher-kinded roles was a big part of the discussion, but there was
 another: superclasses. It's possible that the GND'd class has superclasses
 and that the superclass instances for the original type and the newtype
 are different. If we casted the whole instance, we would get the
 superclass instances from the original type, which would be quite strange.
 Indeed, before making any change related to roles, the old GND code also
 did not cast instances, because of this superclass issue.

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