Opened 12 months ago
Last modified 10 months ago
#15639 new bug
Surprising failure combining QuantifiedConstraints with Coercible
Reported by: | dfeuer | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
I don't understand what's going wrong here.
-- 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 |
Change History (11)
comment:1 Changed 12 months ago by
comment:2 Changed 12 months ago by
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]
.
comment:3 Changed 12 months ago by
Keywords: | QuantifiedConstraints added |
---|
comment:4 Changed 12 months ago by
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.
comment:5 follow-up: 7 Changed 12 months ago by
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.
comment:6 Changed 10 months ago by
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.
comment:7 Changed 10 months ago by
Replying to 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?)
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
data Coercion a b where Coercion :: Coercible a b => Coercion a b
The situation is
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
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.
comment:8 Changed 10 months ago by
Let's go through this 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
- First see if there is a given un-quantified constraint
C t
. If so, use it to solve the constraint.- 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.- 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.
comment:9 Changed 10 months ago by
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.
comment:10 follow-up: 11 Changed 10 months ago by
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.
comment:11 Changed 10 months ago by
Replying to 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?
-ddump-cs-trace
givesI don't know quite how to read this, but I'd have expected
to interact with
and resolve.