Ord1.hs

{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds, PolyKinds, GADTs, RankNTypes, StandaloneKindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Kind

newtype Fix f = Fix (f (Fix f))

    -- Note: a and b
    -- depending on whom you ask this is pro or con


class Eq1 f where
    liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool

instance Eq1 [] where
    liftEq eq = go
      where
        go [] [] = True
        go (x:xs) (y:ys) = eq x y && go xs ys
        go _ _ = False

class Eq1 f => Ord1 f where
    liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering

{-

instance Eq1 f => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = liftEq eq x y

instance Ord1 f => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = liftCompare cmp x y
    
-}

instance (forall x. Eq x => Eq (f x)) => Eq (Fix f) where
    (==) = eq where eq (Fix x) (Fix y) = x == y

instance (forall x. Ord x => Ord (f x), forall x. Eq x => Eq (f x)) => Ord (Fix f) where
    compare = cmp where cmp (Fix x) (Fix y) = compare x y

data Dict :: (k -> Constraint) -> k -> * where
    Dict :: c a => Dict c a

eqInt :: Dict Eq Int
eqInt = Dict

eq1List :: Dict Eq1 []
eq1List = Dict

entail :: Dict Ord1 f -> Dict Eq1 f
entail Dict = Dict

-- eqQList :: Dict (forall x. Eq x => Eq (f x)) []
-- eqQList = undefined

type Eq1' :: (* -> *) -> Constraint
type Eq1' f = forall x. Eq x => Eq (f x)

-- eqQList2 :: Dict Eq1' []
-- eqQList2 = undefined

class Eq1' f => Eq1'' f
instance Eq1' f => Eq1'' f -- needs FlexibleInstances

-- eqQList3 :: Dict Eq1'' f
-- eqQList3 = undefined