Skolem escape at the kind level
This program should be rejected
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE KindSignatures #-}
module Foo2 where
import Data.Kind ( Type )
import Data.Type.Equality
import Data.Proxy
import GHC.Exts
data SameKind :: k -> k -> Type
f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
g = undefined
in ()
But
- 8.0 rejects it, with an unhelpful message
- 8.2 accepts it, and the result satisfies Core Lint
- HEAD accepts it, and produces a Core Lint Error