GitLab

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