Definition of heterogeneous equality rejected unless using a SAKS
The following definitions of heterogeneous equality are rejected on HEAD:
data (a :: k1) :~: (b :: k2) where
HRefl :: a :~~: a
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (a :: k1) :~~: (b :: k2) where
| ^^^^^^^^^^^^^^^^^^^^^^
data (:~~:) :: k1 -> k2 -> Type where
HRefl :: a :~~: a
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
Note that this remains true even if one enables -XCUSKs
, so this doesn't fit the diagnostic of #20752 (comment 394357).
The only way to get this accepted is to write a standalone kind signature:
type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
HRefl :: a :~~: a
It seems to me that the "different names for the same type variable" check is overly-eager for GADTs. In particular, the following is also rejected:
data (:~~:) :: k1 -> k2 -> Type where
NotHRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: b
HRefl :: a :~~: a
error:
* Different names for the same type variable: `k1' and `k2'
* In the data declaration for `:~~:'
|
| data (:~~:) :: k1 -> k2 -> Type where
| ^^^^^^^^
I don't know how GHC concludes that k1
and k2
must refer to the same kind variable there.