Skip to content

GitLab

GHC
GHC
Closed
Opened by Simon Peyton Jones@simonpjDeveloper

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
Edited by Simon Peyton Jones