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