#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