[GHC] #8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles -------------------------------------------+------------------------------- Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Keywords: | Operating System: Architecture: Unknown/Multiple | Unknown/Multiple Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------+------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles --------------------------------------------+------------------------------ Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by haasn): More specifically, the exact type that causes a problem is ‘WrappedSchoenfinkel cat’ and ‘cat’ not being nominally equal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles --------------------------------------------+------------------------------ Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Description changed by simonpj: Old description:
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.
New description: 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles --------------------------------------------+------------------------------ Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Description changed by simonpj: Old description:
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.
New description: 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles --------------------------------------------+------------------------------ Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 simonpj): 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Richard Eisenberg
#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): The patch above does not implement the proposal in comment:6 and agreed to in comment:7. I'll implement this proposal soon, but it will likely miss the 7.10 branch. This is OK -- it won't hurt anyone to have this unfixed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles -------------------------------------+------------------------------------- Reporter: haasn | Owner: goldfire 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: | deriving/should_fail/T8984 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: => goldfire * testcase: => deriving/should_fail/T8984 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type
roles
-------------------------------------+-------------------------------------
Reporter: haasn | Owner: goldfire
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: |
deriving/should_fail/T8984 |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles -------------------------------------+------------------------------------- Reporter: haasn | Owner: goldfire Type: feature | Status: closed request | Milestone: Priority: normal | Version: 7.8.1 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: fixed | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | deriving/should_fail/T8984 | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: All done now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC