Kind inference for newtypes in GADT syntax is deeply broken (#18891) · Issues · Glasgow Haskell Compiler / GHC

Kind inference for newtypes in GADT syntax is deeply broken

Here are some tales of destruction, all with -XUnliftedNewtypes and -XNoCUSKs:

newtype N :: forall k. TYPE k where
  MkN :: N -> N

gives

Scratch.hs:34:3: error:
    • Expected a type, but ‘N’ has kind ‘*’
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’

type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
  MkN :: N -> N

gives

Scratch.hs:35:3: error:
    • A newtype constructor must have a return type of form T a1 ... an
      MkN :: N -> N
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’

newtype N :: forall k -> TYPE k where
  MkN :: N m -> N m

gives

Scratch.hs:35:3: error:
    • Expected a type, but ‘N m’ has kind ‘TYPE m’
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’

type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
  MkN :: N m -> N m

succeeds.

I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.

I think the problem is that the res_kind passed to kcConArgTys has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.

Here are some tales of destruction, all with `-XUnliftedNewtypes` and `-XNoCUSKs`:

```hs
newtype N :: forall k. TYPE k where
  MkN :: N -> N
```

gives

```
Scratch.hs:34:3: error:
    • Expected a type, but ‘N’ has kind ‘*’
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’
```

------------------------

```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
  MkN :: N -> N
```

gives

```
Scratch.hs:35:3: error:
    • A newtype constructor must have a return type of form T a1 ... an
      MkN :: N -> N
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’
```

-------------------------

```hs
newtype N :: forall k -> TYPE k where
  MkN :: N m -> N m
```

gives

```
Scratch.hs:35:3: error:
    • Expected a type, but ‘N m’ has kind ‘TYPE m’
    • In the definition of data constructor ‘MkN’
      In the newtype declaration for ‘N’
```

-------------------------

```hs
type N :: forall k -> TYPE k
newtype N :: forall k -> TYPE k where
  MkN :: N m -> N m
```

succeeds.

I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.

I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.