[GHC] #15639: Surprising failure combining QuantifiedConstraints with Coercible
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I don't understand what's going wrong here. {{{#!hs -- Fishy.hs {-# language RankNTypes, QuantifiedConstraints, RoleAnnotations #-} module Fishy (Yeah, yeahCoercible) where import Data.Coerce data Yeah_ a = Yeah_ Int newtype Yeah a = Yeah (Yeah_ a) type role Yeah representational yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r yeahCoercible r = r -- Fishy2.hs module Fishy2 where import Fishy import Data.Type.Coercion import Data.Coerce yeah :: Coercion [Yeah a] [Yeah b] yeah = yeahCoercible Coercion }}} I get {{{ Fishy2.hs:8:22: error: • Couldn't match representation of type ‘a’ with that of ‘b’ arising from a use of ‘Coercion’ ‘a’ is a rigid type variable bound by the type signature for: yeah :: forall a b. Coercion [Yeah a] [Yeah b] at Fishy2.hs:7:1-34 ‘b’ is a rigid type variable bound by the type signature for: yeah :: forall a b. Coercion [Yeah a] [Yeah b] at Fishy2.hs:7:1-34 • In the first argument of ‘yeahCoercible’, namely ‘Coercion’ In the expression: yeahCoercible Coercion In an equation for ‘yeah’: yeah = yeahCoercible Coercion • Relevant bindings include yeah :: Coercion [Yeah a] [Yeah b] (bound at Fishy2.hs:8:1) | 8 | yeah = yeahCoercible Coercion | }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): `-ddump-cs-trace` gives {{{ Step 1[l:1,d:1] Kept as inert: [WD] hole{co_a11c} {1}:: t_ax2[tau:0] GHC.Prim.~# 'GHC.Types.LiftedRep simpl_loop iteration=0 (no new given superclasses = True, 1 simples to solve) Step 2[l:0,d:1] Solved by unification: [WD] hole{co_a11c} {1}:: t_ax2[tau:0] GHC.Prim.~# 'GHC.Types.LiftedRep Constraint solver steps = 2 Step 1[l:2,d:0] Given forall-constraint: [G] df_a11t {0}:: forall a b. Coercible (Yeah a) (Yeah b) Step 2[l:2,d:0] Decomposed TyConApp: [WD] hole{co_a11z} {0}:: Coercion a_a11w[tau:2] b_a11x[tau:2] GHC.Prim.~# r_a11r[tau:1] Step 3[l:2,d:0] Kept as inert: [WD] hole{co_a11F} {0}:: b_a11x[tau:2] GHC.Prim.~# [Yeah b_a11l[sk:1]] Kick out, tv = k_a11v[tau:2] n-kicked = 1 kicked_out = WL {Eqs = [WD] hole{co_a11F} {0}:: b_a11x[tau:2] GHC.Prim.~# [Yeah b_a11l[sk:1]] (CIrredCan(sol))} Residual inerts = {Given instances = [G] df_a11t {0}:: forall a b. Coercible (Yeah a) (Yeah b) Unsolved goals = 0} Step 4[l:2,d:0] Solved by unification (1 kicked out): [D] _ {0}:: k_a11v[tau:2] GHC.Prim.~# * Step 5[l:2,d:0] Solved by unification: [WD] hole{co_a11F} {0}:: b_a11x[tau:2] GHC.Prim.~# [Yeah b_a11l[sk:1]] Step 6[l:2,d:0] Solved by unification: [WD] hole{co_a11E} {0}:: a_a11w[tau:2] GHC.Prim.~# [Yeah a_a11k[sk:1]] Step 7[l:2,d:0] Solved by reflexivity: [WD] hole{co_a11D} {0}:: k_a11v[tau:2] GHC.Prim.~# * Step 8[l:2,d:0] Dict/Top (solved wanted): [WD] $dCoercible_a11y {0}:: Coercible [Yeah a_a11k[sk:1]] [Yeah b_a11l[sk:1]] Step 9[l:2,d:1] Decomposed TyConApp: [WD] hole{co_a11G} {1}:: [Yeah a_a11k[sk:1]] ~R# [Yeah b_a11l[sk:1]] Step 10[l:2,d:1] Decomposed TyConApp: [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1] Step 11[l:2,d:1] Kept as inert: [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1] Step 12[l:2,d:0] Given forall-constraint: [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b simpl_loop iteration=0 (no new given superclasses = False, 1 simples to solve) Step 13[l:2,d:1] Kept as inert: [WD] hole{co_a11I} {1}:: a_a11k[sk:1] ~R# b_a11l[sk:1] Constraint solver steps = 13 }}} I don't know quite how to read this, but I'd have expected {{{ Step 10[l:2,d:1] Decomposed TyConApp: [WD] hole{co_a11H} {1}:: Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1] }}} to interact with {{{ Step 12[l:2,d:0] Given forall-constraint: [G] df_a11J {0}:: forall a b. Yeah a ~R# Yeah b }}} and resolve. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Best guess: the solver doesn't check for relevant quantified constraints before reducing `Yeah a_a11k[sk:1] ~R# Yeah b_a11l[sk:1]` to `a_a11k[sk:1] ~R# b_a11l[sk:1]`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * keywords: => QuantifiedConstraints -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): If I had to guess, I would guess that there is no entirely satisfactory general solution to this problem. Given `type role F representational` (or `type role F nominal`) and forall a b. `C a b => Coercible (F a) (F b)`, and seeking `Coercible (F a) (F b)` I very much doubt that there's a single optimal way to determine whether to reduce the wanted to `C` or to `Coercible a b` (or `a ~ b`). To be consistent with how this is handled for other classes, we "should" just reject the constraint altogether, as overlapping. But that would be sad, and I do suspect we can do better, at least for some special cases. For example, if we're given `forall a b. Coercible (F a) (F b)`, we want to think of that as improving the type role of `F`'s parameter from whatever it may be to phantom. Similarly, if we're given `forall a b. Coercible a b => Coercible (F a) (F b)`, we want to think of that as improving the type role of `F`s parameter to representational, if it would otherwise be nominal. Adding such special cases to the constraint solver would certainly be a horribly ugly hack, but I don't really know what else we can do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Can you explain more about this example? I think that it is important that * You give a role signature for `Yeah`. (What is the inferred signature?) * You export the type constructor for `Yeah` but not the data constructor. But I'm a bit lost about what you expect to happen. Can you amplify? Why do you think it should typecheck? It'd probably help to give the declaration for `Coercion` too, for those of us who do not use it daily. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by malo): I'm having a similar issue using GHC 8.6.2. Posting as a comment on this ticket since I expect it's related. Here's a minimal example: {{{ -- test.hs {-# LANGUAGE RankNTypes, QuantifiedConstraints #-} import Data.Coerce data Foo i = Foo i data Bar f i = Bar (f i) -- When I ask that we can lift coercions through the functor... class (forall i j. Coercible i j => Coercible (f i) (f j)) => MyFunctor f where -- ... -- ... this works fine. instance MyFunctor Foo -- When I try to ask that we can lift coercions through a higher functor... class (forall f g. (forall i. Coercible (f i) (g i)) => (forall i. Coercible (x f i) (x g i))) => MyHigherFunctor x where -- ... -- ...this fails instance MyHigherFunctor Bar -- Output from ghci: -- -- Prelude> :l test.hs -- [1 of 1] Compiling Main ( test.hs, interpreted ) -- -- test.hs:21:10: error: -- • Couldn't match representation of type ‘f’ with that of ‘g’ -- arising from the superclasses of an instance declaration -- ‘f’ is a rigid type variable bound by -- a quantified context -- at test.hs:1:1 -- ‘g’ is a rigid type variable bound by -- a quantified context -- at test.hs:1:1 -- • In the instance declaration for ‘MyHigherFunctor Bar’ -- | -- 21 | instance MyHigherFunctor Bar -- | ^^^^^^^^^^^^^^^^^^^ -- Failed, no modules loaded. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Can you explain more about this example? I think that it is important
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:5 simonpj]: that
* You give a role signature for `Yeah`. (What is the inferred
signature?) The inferred signature is `type role Yeah phantom`
* You export the type constructor for `Yeah` but not the data constructor.
Yes. The export isn't really as relevant as the import it enables; when a newtype constructor is in scope that changes the coercion axioms the type checker uses for the type.
But I'm a bit lost about what you expect to happen. Can you amplify? Why do you think it should typecheck? It'd probably help to give the declaration for `Coercion` too, for those of us who do not use it daily.
The declaration of `Coercion` is {{{#!hs data Coercion a b where Coercion :: Coercible a b => Coercion a b }}} The situation is {{{#!hs yeahCoercible :: ((forall a b. Coercible (Yeah a) (Yeah b)) => r) -> r yeahCoercible r = r -- Fishy2.hs yeah :: Coercion [Yeah a] [Yeah b] yeah = yeahCoercible Coercion }}} We call `yeahCoercible` with `Coercion`. For this to typecheck, we need {{{#!hs Coercion :: (forall a b. Coercible (Yeah a) (Yeah b)) => Coercion [Yeah a] [Yeah b] }}} Put another way, we need `Coercible (Yeah a) (Yeah b)` to imply `Coercible [Yeah a] [Yeah b]`. Under normal circumstances, that would follow from the fact that `[]`'s parameter has a representational role. But the constraint solver isn't figuring that out. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Let's go through this [http://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.h... #instance-lookup according to the user's guide]:
In the light of the overlap decision, instance lookup works like this when trying to solve a class constraint `C t`
1. First see if there is a given un-quantified constraint `C t`. If so, use it to solve the constraint. 2. If not, look at all the available given quantified constraints; if exactly one one matches `C t`, choose it; if more than one matches, report an error. 3. If no quantified constraints match, look up in the global instances, as described in ...
When type checking the use of the `Coercion` constructor in `yeah`, we want `Coercible [Yeah a] [Yeah b]`. There are no given constraints (quantified or otherwise) matching that, so we use the global instance `Coercible x y => Coercible [x] [y]`, producing the wanted `Coercible (Yeah a) (Yeah b)`. We have no matching unquantified givens, so we look for quantified givens. We (should) have a match: `forall a b. Coercible (Yeah a) (Yeah b)`, which should solve the wanted. However, it ''appears'' that GHC is instead choosing the global instance `forall a b. Coercible a b => Coercible (Yeah a) (Yeah b)`, leading to an unsatisfiable `Coercible a b`. So I don't ''think'' the current behavior matches the user's guide. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): malo, I don't think the problem you're encountering is related at all. You're hoping that `forall i. Coercible (f i) (g i)` will satisfy the `type role Bar representational nominal` requirement. But we don't have such an extensionality rule. Perhaps we could add one somehow, but that would be quite independent. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
So I don't think the current behavior matches the user's guide.
That's probably true. The built-in rules for `Coercible` apply first. So we reduce `Coercible (Yeah a) (Yeah b)` to `Coercible a (Yeah b)` and thence to `Coercible a b`. All this before we even start to consider instances. It's a bit like type-class overlap. GHC doesn't have backtracking, and just picks one path. If you have overlap (as here, in this case between a quantified constraint and a built-in equality-decomposition rule) then GHC just picks one (in this case the built-in rule). The best thing is to avoid overlap. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:10 simonpj]:
The best thing is to avoid overlap.
This is a very good general principle (and the reason I was concerned about bundling implication constraints with quantified constraints). But I think the special case of `Coercible` deserves some special consideration. Overlap is very often (perhaps usually) unavoidable when using quantified constraints with `Coercible`. There's just no way to hide the global mechanism. So I think it pays to consider how we can refine the overlap rules to make these constraints as useful as possible. I ''conjecture'' that we will get strictly or almost strictly better results by applying quantified constraints before and between built-in rules (other than symmetry, which I imagine does some global canonicalization). We seem to already do something special to allow things to work as expected when pattern matching on `Coercion`s to locally reveal `Coercible` instances. Can we do something similar for quantified constraints? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC