() as empty constraint

Question

how can one represent the empty constraint ?

for the following file

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}

import Data.Kind(Type, Constraint)

type Empty = (() :: Type -> Constraint)

main :: IO ()
main = return ()

ghc 8.2.2 answers

constraint.hs:6:15: error:
    • Expected kind ‘* -> Constraint’, but ‘()’ has kind ‘*’
    • In the type ‘(() :: Type -> Constraint)’
      In the type declaration for ‘Empty’
  |
6 | type Empty = (() :: Type -> Constraint)
  |  

what do i miss ?

i know about the following solution

{-# LANGUAGE FlexibleInstances #-}

class Empty x
instance Empty x

but i want to know why () does not work

Answer 1

() has kind * or Constraint, depending on context, never a -> Constraint. Similarly (,) has kind * -> * -> * or Constraint -> Constraint -> Constraint, depending on context.

— Simon Peyton-Jones

It’s just that () is only overloaded for whether it’s a type or a constraint. That is, you’d write () => a, not (() a) => a. So I think this:

class Empty x
instance Empty x

Is the correct solution here. (And perhaps something like that should be in base.)

Answer 2

Jon Purdy's answer is correct. If you want one thing you can slap in regardless of arity (except in an instance head or type family LHS), you're going to need to use some boilerplate:

{-# language PolyKinds, ConstraintKinds, FlexibleInstances,
    MultiParamTypeClasses, TypeFamilies #-}

import Data.Kind (Constraint)

class Unit1 a
instance Unit1 a
class Unit2 a b
instance Unit2 a b
...

type family Unit :: k
type instance Unit = (() :: Constraint)
type instance Unit = Unit1
type instance Unit = Unit2
...

Then

Prelude K> type Empty = (Unit :: Type -> Constraint)
Prelude K> :kind! Empty
Empty :: * -> Constraint
= Unit1

Answer 3

Either of these work fine, depending on what you want:

type Empty = (() :: Constraint)
type ConstEmpty x = (() :: Constraint)

Answer 4

() has kind Constraint and is not meant to be applied to a Type.