Pattern matching on GADT does not refine type family parameters
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)
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |