{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module T10592 where

import Data.Kind (Type)
import Prelude (Bool(True,False),Integer,Ordering)
import qualified Prelude

--------------------
-- class hierarchy

class Boolean (Logic a) => Eq a where
    type Logic a :: Type
    (==) :: a -> a -> Logic a

    (/=) :: a -> a -> Logic a
    a/=b = not (a==b)

class Eq a => POrd a where
    inf :: a -> a -> a

class POrd a => MinBound a where
    minBound :: a

class POrd a => Lattice a where
    sup :: a -> a -> a

class (Lattice a, MinBound a) => Bounded a where
    maxBound :: a

class Bounded a => Complemented a where
    not :: a -> a

class Bounded a => Heyting a where
    infixr 3 ==>
    (==>) :: a -> a -> a

class (Complemented a, Heyting a) => Boolean a

(||) :: Boolean a => a -> a -> a
(||) = sup

(&&) :: Boolean a => a -> a -> a
(&&) = inf

--------------------
-- Bool instances
-- (these work fine)

instance Eq Bool where
    type Logic Bool = Bool
    (==) = (Prelude.==)

instance POrd Bool where
    inf True  True  = True
    inf _     _     = False

instance MinBound Bool where
    minBound = False

instance Lattice Bool where
    sup False False = False
    sup _     _     = True

instance Bounded Bool where
    maxBound = True

instance Complemented Bool where
    not True  = False
    not False = True

instance Heyting Bool where
    False ==> _ = True
    True  ==> a = a

instance Boolean Bool

--------------------
-- Integer instances
-- (these work fine)

instance Eq Integer where
    type Logic Integer = Bool
    (==) = (Prelude.==)

instance POrd Integer where
    inf = Prelude.min

instance Lattice Integer where
    sup = Prelude.max

--------------------
-- function instances
-- (these cause GHC to loop)

instance Eq b => Eq (a -> b) where
    type Logic (a -> b) = a -> Logic b
    f==g = \a -> f a == g a

instance POrd b => POrd (a -> b) where
    inf f g = \a -> inf (f a) (g a)

instance MinBound b => MinBound (a -> b) where
    minBound = \_ -> minBound

instance Lattice b => Lattice (a -> b) where
    sup f g = \a -> sup (f a) (g a)

instance Bounded b => Bounded (a -> b) where
    maxBound = \_ -> maxBound

instance Complemented b => Complemented (a -> b) where
    not f = \a -> not (f a)

instance Heyting b => Heyting (a -> b) where
    f ==> g = \a -> f a ==> g a

instance Boolean b => Boolean (a -> b)