Opened 2 years ago
Closed 17 months ago
#14333 closed bug (fixed)
GHC doesn't use the fact that Coercible is symmetric
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.1 |
Keywords: | TypeFamilies, Roles | Cc: | RyanGlScott |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T14333 |
Blocked By: | Blocking: | ||
Related Tickets: | #14323, #15431 | Differential Rev(s): | |
Wiki Page: |
Description
{-# Language ScopedTypeVariables, GADTs, DeriveGeneric #-} import GHC.Generics import Data.Type.Coercion data AB = A | B deriving (Generic) data XY = X | Y deriving (Generic) data This ab xy where At :: This AB XY foo :: This ab xy -> Coercion (Rep ab a) (Rep xy a) foo At = Coercion bar :: forall ab xy a. This ab xy -> Coercion (Rep ab a) (Rep xy a) bar at | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a) = Coercion
This compiles on 8.2.1 and 8.3.20170920 but flipping the arguments to Coercion
fails
-- ... -- • Could not deduce: Coercible (Rep xy a) (Rep ab a) -- arising from a use of ‘Coercion’ -- from the context: Coercible (Rep ab a) (Rep xy a) -- bound by a pattern with constructor: bar :: forall ab xy a. This ab xy -> Coercion (Rep xy a) (Rep ab a) bar at | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a) = Coercion
Conceptually there should be an (Undecidable
) superclass constraint for Coercible
class Coercible b a => Coercible a b
Attachments (1)
Change History (16)
comment:1 Changed 2 years ago by
Cc: | RyanGlScott added |
---|---|
Keywords: | TypeFamilies added |
comment:2 follow-up: 4 Changed 2 years ago by
This is a good point. The problem is that (a b) ~R# (c d)
tells you nothing at all about the relationship between any of the variables a
, b
, c
, and d
. This isn't a restriction in the solver, but simply a truism of representational equality. So when GHC knows (a b) ~R# (c d)
, it is too stupid to figure out (c d) ~R# (a b)
. I can thus boil down the problem even further:
bad :: Coercible (a b) (c d) => c d -> a b bad = coerce
will fail to type-check. (The version with argument & result swapped works fine.)
Could the solver work around this? Maybe, with sufficient cleverness. (Unlike my concerns around recursive newtypes, I think this may be an engineering issue, not undecidability.) I don't think it would be easy though, requiring some kind of flattening logic akin to what GHC does for type families.
Do you have a concrete use case?
comment:3 Changed 2 years ago by
Keywords: | Roles added |
---|
comment:4 Changed 2 years ago by
Replying to goldfire:
Do you have a concrete use case?
My use case is this where swap
is required to express symmetry. I use this to witness a coercion between Rep a x
and Rep b x
sameRep :: SameRep a b :- (Rep a x `Coercible` Rep b x)
but I also need
SameRep a b :- (Rep b x `Coercible` Rep a x)
for which I use swap
comment:5 Changed 2 years ago by
Could you include the full code of the concrete use case? I followed the link, but that's a non-trivial and not-self-contained file.
GHC accepts
f :: Coercible b a => a x -> b x f = coerce
So, if SameRep a b
implies Coercible (Rep a) (Rep b)
, then the final implication above should hold. If, on the other hand, SameRep a b
implies forall x. Coercible (Rep a x) (Rep b x)
, then you're in trouble (at least with the current implementation).
It occurs to me that you do not necessarily need to do anything clever with a b ~R# c d
, but instead F a b ~R# F c d
, where F
has an arity of 1. Tackling the special case where we have a type function at the head, instead of any variable, might be easier than the general case.
Changed 2 years ago by
Attachment: | SelfContained.hs added |
---|
comment:6 Changed 2 years ago by
I attached an example, I found another need for this: encoding that the opposite category is coercible to the current (based on hask):
type Cat obj = obj -> obj -> Type class (forall xx yy. Coercible (cat xx yy) (Op cat yy xx)) => Category (cat :: Cat obj) where type Op cat :: Cat obj
The use case is similar as the other one but I can elaborate if needed. In my current implementation I want to coerce
between opposite categories but I needed to assume that both directions hold to get both op
& unop
op :: forall cat a b. Category cat => cat a b -> Op cat b a op = coerce \\ coer @cat @a @b unop :: forall cat a b. Category cat => Op cat b a -> cat a b unop = coerce \\ coer @cat @a @b
comment:7 follow-up: 9 Changed 2 years ago by
I found I could do this quite easily. (I happened to be in the area.) Patch coming.
comment:9 Changed 2 years ago by
Replying to simonpj:
I found I could do this quite easily. (I happened to be in the area.) Patch coming.
Ooh. I'm curious. I'm not yet ready to backtrack from my opinion that this would be hard.
comment:11 Changed 2 years ago by
Ooh. I'm curious.
OK, take a look. Most of the patch is good regardless. If you disagree with the payload of the change (matching either way round) it'd be one-line change to take it out again.
comment:12 Changed 2 years ago by
Related Tickets: | → #14323 |
---|
Commit 5a66d574890ed09859ca912c9e0969dba72f4a23 fixed #14323 as well, so if the payload of that commit is reverted, make sure to re-open #14323 as well.
comment:13 Changed 2 years ago by
Your patch solves a smaller problem than I was thinking of... but now I can't seem to think of it again. Regardless, your patch looks correct to me.
comment:14 Changed 17 months ago by
Related Tickets: | #14323 → #14323, #15431 |
---|
Is this bug fixed?
(Also, see #15431 for a possibly related issue.)
comment:15 Changed 17 months ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → typecheck/should_compile/T14333 |
Yes I believe this is fixed
Indeed, something funny is going on here.
Here's a simplified version of this program. Notice that this typechecks:
However, if you change the kind of
F
:Then it no longer typechecks:
Of course, it's quite easy to actually construct an implementation of
f
which does typecheck:So the mystery is why GHC gets tripped up on this particular incarnation of
F
.