[GHC] #14066: Skolem escape at the kind level

[GHC]

#14066: Skolem escape at the kind level
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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

New description:

 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

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14066#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler