[GHC] #11966: Surprising behavior with higher-rank quantification of kind variables

21 Apr 2016

      #11966: Surprising behavior with higher-rank quantification of kind variables
-------------------------------------+-------------------------------------
           Reporter:  ocharles       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1-rc3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Sorry about the rubbish title. I wrote the following code, which type
 checks:

 {{{#!hs
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}

 module Test where

 import Data.Kind (Type)

 -- Simplification
 type family Col (f :: k -> j) (x :: k) :: Type

 -- Base types
 data PGBaseType = PGInteger | PGText

 -- Transformations
 data Column t = Column Symbol t
 newtype Nullable t = Nullable t
 newtype HasDefault t = HasDefault t

 -- Interpretations
 data Expr k

 data Record (f :: forall k. k -> Type) =
   Record {rX :: Col f ('Column "x" 'PGInteger)
          ,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
          ,rZ :: Col f ('HasDefault 'PGText)}

 }}}

 However, if I play with this in GHCI, I can get the following error:

 {{{
 λ> let x = undefined :: Record Expr

 <interactive>:136:29-32: error:
     • Expected kind ‘forall k. k -> Type’,
         but ‘Expr’ has kind ‘forall k. k -> *’
     • In the first argument of ‘Record’, namely ‘Expr’
       In an expression type signature: Record Expr
       In the expression: undefined :: Record Expr
 }}}

 It seems that if I write

 {{{#!hs
 data Expr :: forall k. k -> Type
 }}}

 things work, but I'm unclear if/why that is necessary, and the error
 message certainly needs to be fixed.

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