Opened 3 years ago
Closed 2 years ago
#8984 closed feature request (fixed)
Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles
Reported by: | haasn | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.1 |
Keywords: | Cc: | ||
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | deriving/should_fail/T8984 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
When trying to build acme-schoenfinkel (as an example), I came across an error like this:
Control/Category/Schoenfinkel.hs:66:48: Could not coerce from ‘cat (cat b c, b) c’ to ‘cat (WrappedSchoenfinkel cat b c, b) c’ because ‘cat (cat b c, b) c’ and ‘cat (WrappedSchoenfinkel cat b c, b) c’ are different types. arising from the coercion of the method ‘app’ from type ‘forall b c. cat (cat b c, b) c’ to type ‘forall b c. WrappedSchoenfinkel cat (WrappedSchoenfinkel cat b c, b) c’ Possible fix: use a standalone 'deriving instance' declaration, so you can specify the instance context yourself When deriving the instance for (ArrowApply (WrappedSchoenfinkel cat))
It was not immediately clear to me as a user that this was caused due to it wanting GNT which was now being blocked by type roles (rightfully so, as this instance allows UnsafeCoerce
!), and beyond that, what the specific rule that triggered this was.
In this case the failure is due to WrappedSchoenfinkel cat b c
not being nominally equal to cat b c
, in the type (WrappedSchoenfinkel cat b c, b)
, which is required to be nominally equal to (cat b c, b)
because it's used as a parameter to the variable cat
.
Printing a location breakdown and context information similar to this to the user would help understanding and debugging roles a lot.
Change History (12)
comment:2 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:3 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:4 Changed 3 years ago by
Here's a small test case
{-# 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 ) -- The newtype coercion is N cat ~R cat
We try to prove Coercible (cat (cat Int) (N cat (N cat Int))
. We simplify this (by newtype unrwrapping) to Coercible (cat (cat Int)) (cat (N cat Int))
; and now we are stuck.
T8984.hs:7:46: Could not coerce from ‘cat a (cat a Int)’ to ‘cat a (N cat a Int)’ because ‘cat a (cat a Int)’ and ‘cat a (N cat a Int)’ are different types. arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’
An alternative strategy would be to see that the newtype axiom is over-applied, and instead decompose the application thus:
Coercible (cat (cat Int) (N cat (N cat Int)) ==> (decompose application into two parts) Coercible cat (N cat), cat Int ~ N Cat int
Now the first constraint is soluble, but the second would say something like "cannot deduce cat Int ~ N Cat Int
.
Joachim, Richard, thoughts?
comment:5 Changed 2 years ago by
With my update to the solver (preview available at http://github.com/goldfirere/ghc, wip/rae-new-coercible
branch), the new error message is thus:
T8984.hs:7:46: Couldn't match representation of type ‘cat a (N cat a Int)’ with that of ‘cat a (cat a Int)’ arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ Relevant role signatures: type role N representational nominal nominal NB: We cannot know what roles the parameters to ‘cat a’ have; we must assume that the role is nominal When deriving the instance for (C (N cat a))
I like it, and will close this ticket when I merge.
comment:6 Changed 2 years ago by
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 invalidDerivPred
, 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?
comment:7 Changed 2 years ago by
Yes, I agree with your proposal. We should not blithely accept random (and perhaps unsatisfiable) equality constraints in deriving
contexts. You can always specify the context with standalone-deriving if you want.
Weill you execute on this?
Simon
comment:9 Changed 2 years ago by
comment:10 Changed 2 years ago by
Owner: | set to goldfire |
---|---|
Test Case: | → deriving/should_fail/T8984 |
More specifically, the exact type that causes a problem is
WrappedSchoenfinkel cat
andcat
not being nominally equal.