Opened 11 months ago
Closed 9 months ago
#14938 closed bug (invalid)
Pattern matching on GADT does not refine type family parameters
Reported by: | kcsongor | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.2.2 |
Keywords: | GADTs, TypeFamilies, TypeInType | Cc: | Iceland_jack |
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
Compiling the following code
type family R (x :: k) (y :: k) (prf :: x :~: y) :: x :~: y where R x y Refl = Refl
fails with the error
Temp.hs:49:9: error: • Expected kind ‘x :~: y’, but ‘Refl’ has kind ‘x :~: x’ • In the third argument of ‘R’, namely ‘Refl’ In the type family declaration for ‘R’ | 49 | R x y Refl = Refl | ^^^^
where Refl
is defined as
data a :~: b where Refl :: a :~: a
I would expect pattern-matching on Refl
to bring the equality x ~ y
into scope. It seems like it not only doesn't do that, but the pattern match itself is rejected.
(both 8.2.2 and HEAD)
Attachments (1)
Change History (10)
Changed 11 months ago by
comment:1 follow-up: 4 Changed 11 months ago by
But if you have a type-level Refl
here, then x
and y
really will be the same. The equation you want is R x x Refl = Refl
, like in those other dependently typed languages. If you write a larger example, I can show you how the equation I suggest will work.
comment:2 Changed 11 months ago by
I'd be OK with requiring the user write R x x Refl
. But in that case, the error message is pretty darn misleading. It's complaining about Refl
, but the real error is due to the fact that x
and y
are distinct, right?
comment:3 Changed 11 months ago by
Keywords: | TypeInType added |
---|
I agree that talking about x
and y
would be an improvement, though I wouldn't call the current message wrong...
comment:4 Changed 11 months ago by
Replying to goldfire:
But if you have a type-level
Refl
here, thenx
andy
really will be the same. The equation you want isR x x Refl = Refl
, like in those other dependently typed languages.
In the end I did end up using that equation, but my original idea was to try and avoid non-linear patterns, and passing in an explicit proof seemed like a sensible idea. For example, Idris lets me write
r : x -> y -> x = y -> x = y r x y Refl = Refl
(But of course non-linear patterns are not supported)
Is there something obvious I missed that would explain why this form of matching should not accepted?
comment:5 Changed 11 months ago by
Hm. Maybe it's only Agda that requires you to write a non-linear pattern here. Except that the pattern isn't really non-linear, because the non-linearity (at least in Agda) isn't checked. (Agda has a notation for an argument that has to be a certain way but that isn't checked for when matching.)
In any case, you're right, though. Refl
doesn't bring into scope any coercion. Instead, the appearance of Refl
requires a coercion in order for the equation to match. But because type family equations are at the top level and that there is no phase separation between kind-checking and type-checking, this is all OK. After all, the same type checker that allowed Refl
to be type checked at the type family application site is checking whether the equation matches; if one can prove the types equal, the other can, too.
This design decision does have a few consequences, though. For example, you can't quantify a type family equation over an equality between type family applications: type family F a (pf :: G a :~: H a)
. That just won't work (for several reasons). Of course, it's my hope that we won't have type families in a few years and can use normal GADT pattern matching instead! :)
comment:6 Changed 11 months ago by
Thanks for the explanation! I have encountered that limitation on several occasions, but it never quite clicked; now it makes total sense.
So the only way to match pf
against Refl
is by first providing an a
for which G a
and H a
can actually reduce to the same thing
type family G a where G Int = Nat type family H a where H Int = Nat type family F a (pf :: G a :~: H a) where F Int Refl = True
So it seems like I got the "direction" of the matching wrong. Could you by any chance point me to any resources where this decision is explained in more detail? I skimmed the System FC with Explicit Kind Equality paper, but it wasn't obvious where this would be described.
In any case, I'm happy to close this ticket, as I'm now convinced it's not a bug.
comment:7 Changed 11 months ago by
Cc: | Iceland_jack added |
---|
comment:8 Changed 11 months ago by
No, I can't point you to more discussion -- this was a decision of convenience during implementing. At the time, I hadn't fully noticed all the ramifications of it.
comment:9 Changed 9 months ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
As stated in comment:6, this is by design, and not a bug.
Complete program