Inhabited.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType, GADTs, TypeOperators #-}
module Lib where
import Data.Kind (Type)

data Cat (a :: ()) (b :: ()) where
  MkCat :: Cat '() '()

class Category (k :: t -> t -> Type) where
  identity :: k a a

{-
The following instance doesn't compile:

instance Category Cat where
  identity = MkCat

In order for this to typecheck, we want to ensure that
forall a. Cat a a ~ Cat '() '()

If our type language was total, we could say that
forall (a :: ()). a ~ '()

since '() is the only constructor we have of kind ().


Why does this go wrong?
-}

type family Any :: k


{-
'Any' is a family that takes 0 arguments, and its return kind is 'k', for all
'k'. Let's write some examples:
-}

type Unit1 = (Any :: ())
type Unit2 = (Any Bool Char :: ())
type Unit3 = (Any Bool Any :: ())


{-
All 3 examples have kind (), but none of them is the '() constructor, so we
can't conclude that

forall (a :: ()). a ~ '()


The 'Constrainted Type Families' paper offers the first step towards a solution
to this problem, but it requires a termination checker.
-}