[GHC] #11142: Type-level skolem capture leads to core lint error

27 Nov 2015

      #11142: Type-level skolem capture leads to core lint error
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following ill-typed code is accepted.

 {{{
 {-# LANGUAGE PolyKinds, RankNTypes #-}

 module Bug where

 data SameKind :: k -> k -> *

 foo :: forall b. (forall (a :: k). SameKind a b) -> ()
 foo = undefined
 }}}

 Indeed, Core Lint catches this. But the type-checker should. The problem
 is that `SameKind` forces `a` and `b` to have the same kind. But they
 can't, because `a`'s kind is out of scope at `b`'s binding site. The
 program should be rejected.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11142
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler