CODEWITHSUNDEEP
haskellghcdependent-typeexistential-typedata-kinds
Christopher King
Christopher King

Reputation: 10961

Why aren't existential quantification and datakinds working together?

{-# LANGUAGE DataKinds, ExistentialQuantification, KindSignatures #-}
import Data.Proxy

data Type t= forall (a :: t). Type (Proxy a)

gives the error

Type variable ‘t’ used in a kind
In the kind ‘t’
In the definition of data constructor ‘Type’
In the data declaration for ‘Type’

But t is a Kind variable, not a type variable. What's going on?

Upvotes: 2

Views: 227

Answers (2)

András Kovács
András Kovács

Reputation: 30103

Prior to GHC 8, there are no kind bindings allowed, anywhere. Here, we have to use kind proxies. In this case we can do:

import Data.Proxy

data Type (kp :: KProxy k) = forall (a :: k). Type (Proxy a)

With GHC 8, you can indeed write your original version:

{-# language TypeInType #-}

data Type t = forall (a :: t). Type (Proxy a)

Upvotes: 9

Reid Barton
Reid Barton

Reputation: 15029

The arguments of type constructors are types, not kinds. So data Type t = ... means t is a type variable.

In GHC 8.0 the TypeInType extension removes the distinction between types and kinds, allowing your program to be accepted if you enable it (and GHC will suggest enabling the extension if you don't).

Upvotes: 2

Related Questions