GHC 9.0+ regression in checking program with higher-rank kinds
GHC 8.10.2 typechecks the following program:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type Nat :: Type
data Nat = Z | S Nat
type Vec :: Type -> Nat -> Type
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Z
VCons :: a -> Vec a n -> Vec a (S n)
type ElimVec :: forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type)
-> forall (n :: Nat).
forall (v :: Vec a n)
-> Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
type family ElimVec p v pVNil pVCons where
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)).
ElimVec p VNil pVNil pVCons = pVNil
forall a (p :: forall (k :: Nat). Vec a k ~> Type)
(pVNil :: Apply p VNil)
(pVCons :: forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)) l x xs.
ElimVec p (VCons x (xs :: Vec a l)) pVNil pVCons =
Apply (pVCons x xs) (ElimVec @a p @l xs pVNil pVCons)
However, GHC 9.0.1-alpha1 and HEAD reject it:
$ ~/Software/ghc-9.0.1-alpha1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:26: error:
• Couldn't match kind ‘k1’ with ‘m’
Expected kind ‘Vec a k1’, but ‘xs’ has kind ‘Vec a m’
because kind variable ‘m’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs)’
at Bug.hs:(38,18)-(40,51)
• In the second argument of ‘Apply’, namely ‘xs’
In the first argument of ‘(~>)’, namely ‘Apply p xs’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
40 | Apply p xs ~> Apply p (VCons x xs))
| ^^
Bug.hs:41:25: error:
• Couldn't match kind ‘k0’ with ‘n’
Expected kind ‘Vec a k0’, but ‘v’ has kind ‘Vec a n’
because kind variable ‘n’ would escape its scope
This (rigid, skolem) kind variable is bound by
‘forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v’
at Bug.hs:(35,17)-(41,25)
• In the second argument of ‘Apply’, namely ‘v’
In a standalone kind signature for ‘ElimVec’:
forall a.
forall (p :: forall (k :: Nat). Vec a k ~> Type) ->
forall (n :: Nat).
forall (v :: Vec a n) ->
Apply p VNil
-> (forall (m :: Nat).
forall (x :: a) (xs :: Vec a m) ->
Apply p xs ~> Apply p (VCons x xs))
-> Apply p v
|
41 | -> Apply p v
| ^