Can I parameterise the empty constraint type?

Question

I have a class for queues which allows the instance to define the constraints it places on the elements. For example, a priority queue requires its elements to be orderable:

{-# LANGUAGE MultiParamTypeClasses, ConstraintKinds, FunctionalDependencies #-}

class Queue q c | q -> c where
    empty :: q a
    qpop :: c a => q a -> Maybe (a, q a)
    qpush :: c a => a -> q a -> q a

data PriorityQueue a = ...

instance Queue PriorityQueue Ord where
    ...

This works a charm: inside the instance declaration for PriorityQueue I can operate on elements of the queue using members of Ord such as (>).

---

I've got stuck trying to define a queue which places no requirements on its elements:

newtype LIFO a = LIFO [a]

instance Queue LIFO () where
    empty = LIFO []
    qpop (LIFO []) = Nothing
    qpop (LIFO (x:xs)) = Just (x, LIFO xs)
    qpush x (LIFO xs) = LIFO $ x:xs

This fails, with the following error message from GHC:

The second argument of `Queue' should have kind `* -> Constraint',
  but `()' has kind `*'
In the instance declaration for `Queue LIFO ()'

This error message makes sense to me. Eq accepts a type parameter (we typically write Eq a => ...) whereas () has no parameters - it's a plain old kind mismatch.

---

I had a crack at writing a type function which ignores its second argument, which would allow me to write instance Queue LIFO (Const ()):

{-# LANGUAGE TypeFamilies, KindSignatures, PolyKinds #-}

type family Const a b :: k -> k2 -> k
type instance Const a b = a

I find this interaction of type families and kind polymorphism quite beautiful, so I was rather disappointed when it didn't work (I really thought it would!):

Expecting two more arguments to `a'
The first argument of `Const' should have kind `*',
  but `a' has kind `k0 -> k1 -> k0'
In the type `a'
In the type instance declaration for `Const'

I have a feeling this last example is something stupid like a syntax mistake (I'm new to type families). How can I write a Constraint which doesn't place any restrictions on its argument?

Answer 1

This should work:

class NoConstraint a where
instance NoConstraint a where

instance Queue LIFO NoConstraint where
  ...

The above defines a constraint which is satisfied by all types. As such, the obligations c a where c = NoConstraint can always be discharged. Also, since there are no members in that class, it should have zero (or nearly zero) run-time cost.

The "constraint" () you are trying to use is not seen as an empty constraint set by GHC, but as the unit type () :: *. This causes Const () :: k2 -> *, which triggers the kind error.

If you do not want to use a custom class, you might try e.g. Const (Eq ()) or Const (Num Int), which have the right kind k2 -> Constraint. I do not recommend this, though, since I find it less readable than using a custom class.

(This requires to enable some extensions, as Benjamin Hodgson points out below in a comment.)