{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}


-- (C) 2006, Ralf Lammel
-- Prelude-like type-level functionality


module TypeLevel where

import qualified Prelude

data True
data False
class Bool x
instance Bool True
instance Bool False

class (Bool b, Bool b', Bool b'') => Or b b' b'' | b b' -> b''
instance Or False False False
instance Or False True True
instance Or True False True
instance Or True True True

class (Bool b, Bool b', Bool b'') => And b b' b'' | b b' -> b''
instance And False False False
instance And False True False
instance And True False False
instance And True True True

class IsElem x xs
instance (Elem x xs True) => IsElem x xs

class Bool b => Elem x xs b | x xs -> b
instance Elem x () False
instance (Eq x x' b, Elem x xs b', Or b b' b'') => Elem x (x',xs) b''

class Bool b => SetEq xs ys b | xs ys -> b
instance (SubsetEq xs ys b, SubsetEq ys xs b', And b b' b'') => SetEq xs ys b''

class Bool b => SubsetEq xs ys b | xs ys -> b
instance SubsetEq () ys True
instance (Elem x ys b, SubsetEq xs ys b', And b b' b'') => SubsetEq (x,xs) ys b''

class Nub x y | x -> y
instance Nub () ()
instance (Nub x' y, Elem x y b, Nub' b x y y') => Nub (x,x') y'
class Bool b => Nub' b x y y' | b x y -> y'
instance Nub' True x y y
instance Nub' False x y (x,y)

class Diff xs ys zs | xs ys -> zs
instance Diff xs () xs
instance (Sub xs y xs', Diff xs' ys zs) => Diff xs (y,ys) zs

class Sub xs y xs' | xs y -> xs'
instance Sub () y ()
instance (Eq x y b, Sub' b x xs y xs') => Sub (x,xs) y xs'
class Sub' b x xs y xs' | b x xs y -> xs'
instance Sub xs y xs' => Sub' False x xs y (x,xs')
instance Sub xs y xs' => Sub' True x xs y xs'

class Append xs ys zs | xs ys -> zs
instance Append () ys ys
instance Append xs ys zs => Append (x,xs) ys (x,zs)

class Concat xss xs | xss -> xs
instance Concat () ()
instance (Concat xss xs', Append xs xs' xs'') => Concat (xs,xss) xs''

class Cast   a b   | a -> b, b -> a   where typeCast   :: a -> b
class Cast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class Cast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance Cast'  () a b => Cast a b where typeCast x = typeCast' () x
instance Cast'' t a b => Cast' t a b where typeCast' = typeCast''
instance Cast'' () a a where typeCast'' _ x  = x

class Eq' () x y b => Eq x y b | x y -> b
class Eq' q x y b | q x y -> b
class Eq'' q x y b | q x y -> b
instance Eq' () x y b => Eq x y b
instance Cast b True => Eq' () x x b
instance Eq'' q x y b => Eq' q x y b
instance Eq'' () x y False