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

 Replying to [comment:5 simonpj]:
 >
 > Moreover, doesn't your example work perfectly well without eta
 reduction?  To typecheck the `deriving instance` we need
 > {{{
 >   IdentityT [] Int  ~R  IdentityT MyList Int
 > }}}
 > Now, using the `Coercible` instances in Fig 2 of
 [http://research.microsoft.com/en-
 us/um/people/simonpj/papers/ext-f/coercible.pdf the paper], we can reduce
 that to
 > {{{
 >   [Int] ~R  MyList Int
 > }}}
 > and that is true with the non-eta-reduced axiom.
 >
 > If `IdentityT`'s data constructor was not in scope, then indeed the
 program will still typecheck -- but arguably doing so exposes something
 about the representation of the newtype, harming abstraction.  You
 certainly couldn't have written it be hand.

 I hadn't considered the newtype-unwrapping axiom when writing the example.
 You're right -- we don't need eta reduction. But, if `IdentityT` were a
 ''data''type instead of a newtype, we would, without further changes to
 the example. The "harming abstraction" note is exactly the debate about
 whether or not we should be able to coerce `Map String Int` to `Map String
 Age` without `Map`'s constructor being in scope.

 >
 > It all seems quite debatable to me.  Do we really want a significant
 cluster of complexity in the implementation, to implement an un-documented
 feature, which no one is asking for, and whose very existence is
 debatable?

 It still makes me nervous to reduce expressiveness -- I just don't want
 users of 7.10 to suddenly lose something, post here that they need it
 back, and then have it restored for 7.12, leaving a lot of CPP in their
 code.

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