Kind inference with SigTvs is wrong (#11203) · Issues · Glasgow Haskell Compiler / GHC

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 SigTvs for user-written kind variables. SigTvs are allowed to unify with other SigTvs, 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

Consider

```hs
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:

```hs
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, but that example has a CUSK and thus works. The bug can happen only when there is no CUSK.

<details><summary>Trac metadata</summary>

| 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           |              |

</details>