{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators,
             DefaultSignatures, ScopedTypeVariables, InstanceSigs,
             MultiParamTypeClasses, FunctionalDependencies,
             UndecidableInstances, CPP, TypeApplications #-}
{-# OPTIONS_GHC -Wno-missing-signatures -Wno-orphans #-}

#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif

#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module ByHand2 where

import Data.Kind
import Data.Singletons (Sing)

#if __GLASGOW_HASKELL__ >= 810
type Nat :: Type
#endif
data Nat = Zero | Succ Nat

#if __GLASGOW_HASKELL__ >= 810
type SNat :: Nat -> Type
#endif
data SNat :: Nat -> Type where
  SZero :: SNat 'Zero
  SSucc :: SNat n -> SNat ('Succ n)
#if __GLASGOW_HASKELL__ >= 808
type instance Sing @Nat =
#else
type instance Sing =
#endif
  SNat

{-
type Bool :: Type
data Bool = False | True
-}

#if __GLASGOW_HASKELL__ >= 810
type SBool :: Bool -> Type
#endif
data SBool :: Bool -> Type where
  SFalse :: SBool 'False
  STrue  :: SBool 'True
#if __GLASGOW_HASKELL__ >= 808
type instance Sing @Bool =
#else
type instance Sing =
#endif
  SBool

{-
type Ordering :: Type
data Ordering = LT | EQ | GT
-}

#if __GLASGOW_HASKELL__ >= 810
type SOrdering :: Ordering -> Type
#endif
data SOrdering :: Ordering -> Type where
  SLT :: SOrdering 'LT
  SEQ :: SOrdering 'EQ
  SGT :: SOrdering 'GT
#if __GLASGOW_HASKELL__ >= 808
type instance Sing @Ordering =
#else
type instance Sing =
#endif
  SOrdering

{-
not :: Bool -> Bool
not True  = False
not False = True
-}

#if __GLASGOW_HASKELL__ >= 810
type Not :: Bool -> Bool
#endif
type family Not (x :: Bool) :: Bool where
  Not 'True = 'False
  Not 'False = 'True

sNot :: Sing b -> Sing (Not b)
sNot STrue = SFalse
sNot SFalse = STrue

{-
type Eq :: Type -> Constraint
class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  infix 4 ==, /=

  x == y = not (x /= y)
  x /= y = not (x == y)
-}

#if __GLASGOW_HASKELL__ >= 810
type PEq :: Type -> Constraint
#endif
class PEq a where
  type (==) (x :: a) (y :: a) :: Bool
  type (/=) (x :: a) (y :: a) :: Bool

  type x == y = Not (x /= y)
  type x /= y = Not (x == y)

#if __GLASGOW_HASKELL__ >= 810
type SEq :: Type -> Constraint
#endif
class SEq a where
  (%==) :: Sing (x :: a) -> Sing (y :: a) -> Sing (x == y)
  (%/=) :: Sing (x :: a) -> Sing (y :: a) -> Sing (x /= y)

  default (%==) :: ((x == y) ~ (Not (x /= y))) => Sing (x :: a) -> Sing (y :: a) -> Sing (x == y)
  x %== y = sNot (x %/= y)

  default (%/=) :: ((x /= y) ~ (Not (x == y))) => Sing (x :: a) -> Sing (y :: a) -> Sing (x /= y)
  x %/= y = sNot (x %== y)

instance Eq Nat where
  Zero == Zero = True
  Zero == Succ _ = False
  Succ _ == Zero = False
  Succ x == Succ y = x == y

instance PEq Nat where
  type 'Zero   == 'Zero   = 'True
  type 'Succ x == 'Zero   = 'False
  type 'Zero   == 'Succ x = 'False
  type 'Succ x == 'Succ y = x == y

instance SEq Nat where
  (%==) :: forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (x == y)
  SZero   %== SZero   = STrue
  SSucc _ %== SZero   = SFalse
  SZero   %== SSucc _ = SFalse
  SSucc x %== SSucc y = x %== y

{-
instance Eq Ordering where
  LT == LT = True
  LT == EQ = False
  LT == GT = False
  EQ == LT = False
  EQ == EQ = True
  EQ == GT = False
  GT == LT = False
  GT == EQ = False
  GT == GT = True
-}

instance PEq Ordering where
  type 'LT == 'LT = 'True
  type 'LT == 'EQ = 'False
  type 'LT == 'GT = 'False
  type 'EQ == 'LT = 'False
  type 'EQ == 'EQ = 'True
  type 'EQ == 'GT = 'False
  type 'GT == 'LT = 'False
  type 'GT == 'EQ = 'False
  type 'GT == 'GT = 'True

instance SEq Ordering where
  SLT %== SLT = STrue
  SLT %== SEQ = SFalse
  SLT %== SGT = SFalse
  SEQ %== SLT = SFalse
  SEQ %== SEQ = STrue
  SEQ %== SGT = SFalse
  SGT %== SLT = SFalse
  SGT %== SEQ = SFalse
  SGT %== SGT = STrue

{-
type Ord :: Type -> Constraint
class Eq a => Ord a where
  compare :: a -> a -> Ordering
  (<) :: a -> a -> Bool

  x < y = compare x y == LT
-}

#if __GLASGOW_HASKELL__ >= 810
type POrd :: Type -> Constraint
#endif
class PEq a => POrd a where
  type Compare (x :: a) (y :: a) :: Ordering
  type (<) (x :: a) (y :: a) :: Bool

  type x < y = Compare x y == 'LT

#if __GLASGOW_HASKELL__ >= 810
type SOrd :: Type -> Constraint
#endif
class SEq a => SOrd a where
  sCompare :: Sing (x :: a) -> Sing (y :: a) -> Sing (Compare x y)
  (%<) :: Sing (x :: a) -> Sing (y :: a) -> Sing (x < y)

  default (%<) :: ((x < y) ~ (Compare x y == 'LT)) => Sing (x :: a) -> Sing (y :: a) -> Sing (x < y)
  x %< y = sCompare x y %== SLT

instance Ord Nat where
  compare Zero Zero = EQ
  compare Zero (Succ _) = LT
  compare (Succ _) Zero = GT
  compare (Succ a) (Succ b) = compare a b

instance POrd Nat where
  type Compare 'Zero     'Zero     = 'EQ
  type Compare 'Zero     ('Succ x) = 'LT
  type Compare ('Succ x) 'Zero     = 'GT
  type Compare ('Succ x) ('Succ y) = Compare x y

instance SOrd Nat where
  sCompare SZero SZero = SEQ
  sCompare SZero (SSucc _) = SLT
  sCompare (SSucc _) SZero = SGT
  sCompare (SSucc x) (SSucc y) = sCompare x y

#if __GLASGOW_HASKELL__ >= 810
type Pointed :: Type -> Constraint
#endif
class Pointed a where
  point :: a

#if __GLASGOW_HASKELL__ >= 810
type PPointed :: Type -> Constraint
#endif
class PPointed a where
  type Point :: a

#if __GLASGOW_HASKELL__ >= 810
type SPointed :: Type -> Constraint
#endif
class SPointed a where
  sPoint :: Sing (Point :: a)

instance Pointed Nat where
  point = Zero

instance PPointed Nat where
  type Point = 'Zero

instance SPointed Nat where
  sPoint = SZero

--------------------------------

#if __GLASGOW_HASKELL__ >= 810
type FD :: Type -> Type -> Constraint
#endif
class FD a b | a -> b where
  meth :: a -> a
  l2r  :: a -> b

instance FD Bool Nat where
  meth = not
  l2r False = Zero
  l2r True = Succ Zero

t1 = meth True
t2 = l2r False

#if __GLASGOW_HASKELL__ >= 810
type PFD :: Type -> Type -> Constraint
#endif
class PFD a b | a -> b where
  type Meth (x :: a) :: a
  type L2r (x :: a) :: b

instance PFD Bool Nat where
  type Meth a = Not a
  type L2r 'False = 'Zero
  type L2r 'True = 'Succ 'Zero

type T1 = Meth 'True

#if __GLASGOW_HASKELL__ >= 810
type T2 :: Nat
#endif
type T2 = (L2r 'False :: Nat)

#if __GLASGOW_HASKELL__ >= 810
type SFD :: Type -> Type -> Constraint
#endif
class SFD a b | a -> b where
  sMeth :: forall (x :: a). Sing x -> Sing (Meth x :: a)
  sL2r :: forall (x :: a). Sing x -> Sing (L2r x :: b)

instance SFD Bool Nat where
  sMeth x = sNot x
  sL2r SFalse = SZero
  sL2r STrue = SSucc SZero

sT1 = sMeth STrue
sT2 :: Sing T2
sT2 = sL2r SFalse