Surprising behavior with higher-rank quantification of kind variables
Sorry about the rubbish title. I wrote the following code, which type checks:
{-# 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
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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1-rc3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |