#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles -------------------------------------+------------------------------------- Reporter: haasn | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.1 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Refactoring in my branch has added a small wrinkle here: my version currently ''accepts'' the original code. Let's be concrete: {{{ {-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-} module T8984 where class C a where app :: a (a Int) newtype N cat a b = MkN (cat a b) deriving( C ) }}} yields an instance {{{ instance (Coercible (cat a (N cat a Int)) (cat a (cat a Int)), C (cat a)) => C (N cat a) }}} This is actually perfectly sound: GHC is just choosing to abstract over the unprovable `Coercible` constraint. What do we think of this behavior? Is it desired or not? This seems to be a free choice here: I don't think either option or the other would affect much else. Implementation note: This is a direct consequence of changes to `TcValidity.validDerivPred`. Previously (that is, in today's HEAD), a `Coercible` constraint looked like a class constraint, meaning it was checked to make sure that it wasn't too exotic. In my branch, (`wip/rae- new-coercible`) `Coercible` constraints are like equalities, which are allowed unchecked. Thus, the rather exotic constraint above is allowed. This has all gotten me thinking: Why ''do'' we blithely allow equality constraints to be in a derived-inferred context? This ability was added in response to #6088, where the user wanted to use GND to derive an instance based on another instance with an explicit equality in the context. Here is the example from #6088: {{{ class C a newtype A n = A Int type family Pos n data True instance (Pos n ~ True) => C (A n) newtype B n = B (A n) deriving (C) }}} This is now accepted. However, here is a very similar case: {{{ class C1 a b class C2 a instance C1 a a => C2 (Maybe a) newtype N a = MkN (Maybe a) deriving C2 }}} This second case is rejected. And yet, they're similar in that the exotic context that might be inferred is specified by the user. It seems a little odd to accept one and reject the other. So, I propose the following behavior: * Reject equality constraints to be inferred for `deriving`. * If `deriving` failed solely because of checks in `validDerivPred`, provide the full inferred context in the error message to make it easy for users to work around this restriction. This would, essentially, break the fix for #6088, and would thus be a regression, because 7.8 incorporates the #6088 fix. But, with the enhanced error message, the breakage would be easy to fix. What do folks think? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler