[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 <eir@…>): In [changeset:"0cc47eb90805f3e166ac4d3991e66d3346ca05e7/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="0cc47eb90805f3e166ac4d3991e66d3346ca05e7" Rewrite `Coercible` solver Summary: This is a rewrite of the algorithm to solve for Coercible "instances". A preliminary form of these ideas is at https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver The basic idea here is that the `EqPred` constructor of `PredTree` now is parameterised by a new type `EqRel` (where `data EqRel = NomEq | ReprEq`). Thus, every equality constraint can now talk about nominal equality (the usual case) or representational equality (the `Coercible` case). This is a change from the previous behavior where `Coercible` was just considered a regular class with a special case in `matchClassInst`. Because of this change, representational equalities are now canonicalized just like nominal ones, allowing more equalities to be solved -- in particular, the case at the top of #9117. A knock-on effect is that the flattener must be aware of the choice of equality relation, because the inert set now stores both representational inert equalities alongside the nominal inert equalities. Of course, we can use representational equalities to rewrite only within another representational equality -- thus the parameterization of the flattener. A nice side effect of this change is that I've introduced a new type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness in the flattener. This commit includes some refactoring as discussed on D546. It also removes the ability of Deriveds to rewrite Deriveds. This fixes bugs #9117 and #8984. Reviewers: simonpj, austin, nomeata Subscribers: carter, thomie Differential Revision: https://phabricator.haskell.org/D546 GHC Trac Issues: #9117, #8984 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8984#comment:8> 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): 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 <eir@…>): In [changeset:"02b4845e07ef7110b2f735f323eb8748903330ff/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="02b4845e07ef7110b2f735f323eb8748903330ff" Consider equality contexts exotic, uninferrable by "deriving" See comments in #8984. This takes back the fix for #6088. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8984#comment:11> 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: 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