Kind inference with SigTvs is wrong
Consider
data SameKind :: k -> k -> *
data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
This code should be rejected. Yet it is accepted. The problem is that, when kind-checking a datatype declaration without a CUSK, GHC uses SigTv
s for user-written kind variables. SigTv
s are allowed to unify with other SigTv
s, leading to incorrect behavior here.
The motivating scenario is this:
data T (a :: k1) x = MkT (S a ())
data S (b :: k2) y = MkS (T b ())
This program should be accepted. Neither type has a CUSK and therefore is not generalized before kind-checking the group. GHC must then unify k1
and k2
. If they were skolems, this unification would fail and this pair of definitions would be rejected.
This ticket is identical in spirit to #9201 (closed), but that example has a CUSK and thus works. The bug can happen only when there is no CUSK.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |