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

31 Jul 2017


      #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