{-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies,
    FlexibleInstances, UndecidableInstances, TypeOperators, TypeFamilies, 
    GADTs, ConstraintKinds, ScopedTypeVariables, FlexibleContexts, 
    EmptyDataDecls, KindSignatures, Rank2Types, PolyKinds, 
    LiberalTypeSynonyms, OverlappingInstances #-}

-- | A Prelude for type-level programming with type classes
-- 
-- This module includes a partial port of the Prelude as type class
-- predicates and pseudo-syntax for case/if-then-else/lambda.
-- 
-- TODO:
-- 
--  - Lambda is useless because the variables are not copied.
--    I need some form of prolog's copy_term.
-- 
--  - Type families don't match if the kinds are too polymorphic,
--    see example for Compose.
-- 
--  - Match and Case need some fine tuning.
-- 
--  - Once the solver for Nat works, implement Num Nat and
--    changes some uses of Integer to Nat
-- 
--  - The GHC Constraint solver doesn't seem to flatten tuple
--    constraints, which sometimes causes it to diverge. For some complex
--    constraints C,
--        C => a        converges but
--        ((), C) => a  diverges

module Prelude.Type (
  module Prelude,
  module Prelude.Type,
  module GHC.Prim,
  module GHC.TypeLits,
  module Prelude.Type.Match,
  module Prelude.Type.Integer,
  module Prelude.Type.Value
  ) where

import Prelude.Type.Match
import Prelude.Type.Integer
import Prelude.Type.Value
import qualified Prelude.Type.Families as F

import Prelude(
  Bool(False, True),
  Maybe(Nothing, Just),
  Either(Left, Right),
  Ordering(LT, GT, EQ)
  )

import GHC.TypeLits (Symbol, Nat)

import GHC.Prim (Constraint)

-- * Syntax emulation

-- | Lambda

-- TODO: Lambda is useless without copy_term

class Lambda1 (a :: k) (c :: Constraint) (a' :: k) | a' c -> a
instance c => Lambda1 a c a
class Lambda2 (a :: k1) (b :: k2) (c :: Constraint) (a' :: k1) (b' :: k2) | a' b' c -> a b
instance c => Lambda2 a b c a b
class Lambda3 (a :: k1) (b :: k2) (d :: k3) (c :: Constraint) (a' :: k1) (b' :: k2) (d' :: k3) | a' b' d' c -> a b d
instance c => Lambda3 a b d c a b d
class Lambda4 (a :: k1) (b :: k2) (d :: k3) (e :: k4) (c :: Constraint) (a' :: k1) (b' :: k2) (d' :: k3) (e' :: k4) | a' b' d' e' c -> a b d e
instance c => Lambda4 a b d e c a b d e

type family Lambda :: k
type instance Lambda = Lambda1
type instance Lambda = Lambda2
type instance Lambda = Lambda3
type instance Lambda = Lambda4

-- | If Then Else

-- >>> T :: If (I 3 < I 4) (x ~ "a") (x ~ "b") => T x
-- "a"
class If (p :: Bool -> Constraint) (a :: Constraint) (b :: Constraint)
instance (p x, F.If x a b) => If p a b 

-- | Case

-- Variable matching in a Case alternative only works if
-- Prelude.Type.Match is compiled with IncoherentInstances, but it
-- causes many bugs elsewhere so it is turned off.
--
-- >>> T :: Case (Just (I 1)) '[Just i --> x ~ i, Nothing --> x ~ I 0] => T x
-- 1
-- >>> T :: Case (Just (I 1)) '[Nothing --> x ~ I 0, Just i --> x ~ i] => T x
-- 1
class Case (a :: k) (c :: [Alternative k Constraint])
instance Error '("Case: No matching alternative for", a) => Case a '[]
instance b => Case a ('[Otherwise b])
instance (Match a x p, Case' p b a cs) => Case a ((x --> b) ': cs)
class Case' (p :: Bool) (b :: Constraint) (a :: k) (cs :: [Alternative k Constraint])
instance b => Case' True b a cs
instance Case a cs => Case' False b a cs

data Alternative a b = (-->) a b | Otherwise b

-- * Type Classes

-- ** Show

class Show (a :: k) (b :: [Symbol]) | a -> b
instance Shows a '[] b => Show a b

class Shows (a :: k) (b :: [Symbol]) (c :: [Symbol]) | a b -> c

-- TODO: ShowsPrec

-- ** Kind

-- | Get kind of a type

class Kind (a :: k) (k' :: *) | k -> k', k' -> k

-- ** Eq

class ((a :: k) == (b :: k)) (p :: Bool) | a b -> p

class ((a :: k) /= (b :: k)) (p :: Bool) | a b -> p
instance ((a == b) p, Not p q) => (a /= b) q

-- ** Ord

class Compare (a :: k) (b :: k) (o :: Ordering) | a b -> o

class ((a :: k) < (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
          Case o [LT --> True ~ p,
                  Otherwise (False ~ p)])
         => (a < b) p

class ((a :: k) <= (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
          Case o [GT --> False ~ p,
                  Otherwise (True ~ p)])
         => (a <= b) p

class ((a :: k) >= (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
          Case o [LT --> False ~ p,
                  Otherwise (True ~ p)])
         => (a >= b) p

class ((a :: k) > (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
          Case o [GT --> True ~ p,
                  Otherwise (False ~ p)])
         => (a > b) p

class Max (a :: k) (b :: k) (max :: k)
instance (Compare a b o,
          Case o [
             LT --> (max ~ b),
             Otherwise (max ~ a)]) 
         => Max a b max

class Min (a :: k) (b :: k) (min :: k)
instance (Compare a b o,
          Case o [
             GT --> (min ~ b),
             Otherwise (min ~ a)]) 
         => Min a b min

-- ** Enum
          
-- >>> T :: ToEnum (I 1) a => T (a :: Ordering)
-- EQ
-- >>> T :: ToEnum (I 1) a => T (a :: Bool)
-- True
class ToEnum (i :: Integer) (a :: k) | k i -> a

class FromEnum (a :: k) (i :: Integer) | a -> i

class Succ (a :: k) (b :: k) | a -> b
instance (FromEnum a i, (i + I 1) j, ToEnum j b) => Succ a b

class Pred (a :: k) (b :: k) | a -> b
instance (FromEnum a i, (i `Minus` I 1) j, ToEnum j b) => Pred a b

-- >>> T::T (EnumFromTo LT GT)
-- [LT,EQ,GT]
class EnumFromTo (a :: k) (b :: k) (l :: [k]) | a b -> l
instance (FromEnum a i,
          FromEnum b j,
          EnumFromTo i j k,
          Map ToEnum k l)
         => EnumFromTo a b l

-- >>> T::T (EnumFromTo (I 5) (I 8))
-- [5,6,7,8]
instance If (b < a) (l ~ '[])
            (((I 1) + a) c, EnumFromTo c b k, l ~ (a ': k))
         => EnumFromTo (a :: Integer) b l

-- >>> T::T (EnumFromThenTo (Just (I 5)) (Just (I 9)) (Just (I 14)))
-- [Just 5,Just 9,Just 13]
class EnumFromThenTo (a :: k) (c :: k) (b :: k) (l :: [k]) | a c b -> l
instance (FromEnum a i,
          FromEnum c h,
          FromEnum b j,
          EnumFromThenTo i h j k,
          Map ToEnum k l)
         => EnumFromThenTo a c b l

-- >>> T :: EnumFromThenTo (I 5) (I 9) (I 14) k => T k
-- [5,9,13]
instance ((c `Minus` a) x, EnumFromToBy a b x l)
         => EnumFromThenTo (a :: Integer) c b l

class EnumFromToBy (a :: k) (b :: k) (c :: k) (l :: [k]) | a b c -> l
instance If (b < a) (l ~ '[])
             ((c + a) d, EnumFromToBy d b c k, l ~ (a ': k))
  => EnumFromToBy a b c l

-- ** Bounded

class MinBound (a :: k) | k -> a
instance F.MinBound ~ a => MinBound a

class MaxBound (a :: k) | k -> a
instance F.MaxBound ~ a => MaxBound a

-- * Primitive kinds

-- ** Unit

instance Shows '() x ("()" ': x)

instance ToEnum Zeros '()
instance FromEnum '() Zeros

instance Kind '() ()

instance ((a :: ()) == b) True

instance Compare '() '() EQ

-- ** Maybe

instance Shows Nothing x ("Nothing" ': x)
instance Shows a x y => Shows (Just a) x ("Just" ': y)

instance FromEnum Nothing Zeros
instance (FromEnum a i, (i + I 1) j) => FromEnum (Just a) j

-- >>> T :: ToEnum (I 1) a => T (a :: Maybe Integer)
-- Just 0
instance ToEnum Zeros Nothing
instance ((j `Minus` I 1) i, ToEnum i a, e ~ Just a) => ToEnum j e

instance Compare Nothing Nothing EQ
instance Compare Nothing (Just a) LT
instance Compare (Just a) Nothing GT
instance Compare a b o => Compare (Just a) (Just b) o

instance Kind a k => Kind (Just a) (Maybe k)
instance Kind Nothing (Maybe k)

instance               (Nothing == Nothing) True
instance (a == b) p => (Just a  == Just b)  p
instance               (Nothing == Just b)  False
instance               (Just a  == Nothing) False

-- ** Bool

instance Shows True x ("True" ': x)
instance Shows False x ("False" ': x)

instance FromEnum False Zeros
instance FromEnum True (One Zeros)

instance ToEnum Zeros False
instance ToEnum (One Zeros) True

instance o ~ (F.Compare a b) => Compare (a :: Bool) b o

instance Kind (a :: Bool) Bool

instance p ~ (a F.== b) => ((a :: Bool) == b) p

class Not (a :: Bool) (b :: Bool) | a -> b
instance Not True False
instance Not False True

class ((a :: Bool) || (b :: Bool)) (c :: Bool) | a b -> c
instance (False || False) False
instance True ~ p => (a || b) p

class ((a :: Bool) && (b :: Bool)) (c :: Bool) | a b -> c
instance (True && True) True
instance False ~ p => (a && b) p

-- ** Ordering

instance y ~ F.Shows o x => Shows (o :: Ordering) x y

instance i ~ F.FromEnum o => FromEnum (o :: Ordering) i

instance o ~ F.ToEnum i => ToEnum i o

instance o ~ F.Compare a b => Compare (a :: Ordering) b o

instance Kind (a :: Ordering) Ordering

instance TypeEq a b p => ((a :: Ordering) == b) p

-- ** Either

instance Shows a x y => Shows (Left a) x ("Left" ': y)
instance Shows a x y => Shows (Right a) x ("Right" ': y)

instance Compare (Left a) (Right b) LT
instance Compare (Right a) (Left b) GT
instance Compare a b o => Compare (Right a) (Right b) o
instance Compare a b o => Compare (Left a) (Left b) o

-- TODO: l is ambiguous
instance Kind a k => Kind (Left a) (Either k l)
instance Kind a k => Kind (Right a) (Either l k)

instance (a == b) p => (Left a  == Left b)  p
instance (a == b) p => (Right a == Right b) p
instance               (Left a  == Right b) False
instance               (Right a  == Left b) False

-- ** Tuples

instance (Shows a ("," ': y) z, Shows b (")" ': x) y)  => Shows '(a, b) x ("(" ': z)
instance (Shows a ("," ': y) z, Shows b ("," ': x) y, Shows c (")" ': w) x)  => Shows '(a, b, c) w ("(" ': z)
instance (Shows a ("," ': y) z, Shows b ("," ': x) y, Shows c ("," ': w) x, Shows d (")" ': v) w)  => Shows '(a, b, c, d) v ("(" ': z)

instance
  (Compare a e o,
   Case o [
    EQ --> Compare b f r,
    o --> o ~ r
   ])
  => Compare '(a, b) '(e, f) r
instance
  (Compare a e o,
   Case o [
    EQ --> Compare '(b, c) '(f, g) r,
    o --> o ~ r
   ])
  => Compare '(a, b, c) '(e, f, g) r
instance
  (Compare a e o,
   Case o [
    EQ --> Compare '(b, c, d) '(f, g, h) r,
    o --> o ~ r
   ])
  => Compare '(a, b, c, d) '(e, f, g, h) r

instance (Kind a k, Kind b l) => Kind '(a, b) (k, l)
instance (Kind a k, Kind b l, Kind c m) => Kind '(a, b, c) (k, l, m)
instance (Kind a k, Kind b l, Kind c m, Kind d n) => Kind '(a, b, c, d) (k, l, m, n)

instance ((a == w) p, (b == x) q, (p && q) o) =>
         ('(a, b) == '(w, x)) o
instance ((a == w) p, (b == x) q, (c == y) r, (p && q) n, (n && r) p) =>
         ('(a, b, c) == '(w, x, y)) o
instance ((a == w) p, (b == x) q, (c == y) r, (d == z) s,
          (p && q) m, (r && s) n, (m && n) o) =>
    ('(a, b, c, d) == '(w, x, y, z)) o

class Fst (p :: (a, b)) (x :: a) | p -> x
instance Fst '(a, b) a

class Snd (p :: (a, b)) (x :: b) | p -> x
instance Snd '(a, b) b

-- ** Type Literals

instance Shows (a :: Symbol) x (a ': x)

instance Kind (a :: Nat) Nat
instance Kind (a :: Symbol) Symbol

instance TypeEq a b p => ((a :: Nat) == b) p
instance TypeEq a b p => ((a :: Symbol) == b) p

-- ** Star

-- | The Kind *

data StarKind

instance Kind (a :: *) StarKind

instance TypeEq a b p => ((a :: *) == b) p

-- * Predicates/Constraints

-- >>> T :: Compose1 Succ Succ (I 1) a => T a
-- 3
class Compose1 (f :: k -> l -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) | f g -> x z
instance (g x y, f y z) => Compose1 f g x z
class Compose2 (f :: k -> l -> m -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) | f g -> x z
instance (g x y, f y z a) => Compose2 f g x z a
class Compose3 (f :: k -> l -> m -> n -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) (b :: n) | f g -> x z
instance (g x y, f y z a b) => Compose3 f g x z a b
class Compose4 (f :: k -> l -> m -> n -> o -> Constraint) (g :: j -> k -> Constraint) (x :: j) (z :: l) (a :: m) (b :: n) (c :: o) | f g -> x z
instance (g x y, f y z a b c) => Compose4 f g x z a b c

type O = Compose


-- >>> T :: Compose Succ Succ (I 1) a => T a
-- ERROR: Could not deduce (Compose ...)
-- >>> T :: Compose (Succ :: Integer -> Integer -> Constraint) (Succ :: Integer -> Integer -> Constraint) (I 1) (a :: Integer) => T a
-- 3
type family Compose :: k
type instance Compose = Compose1
type instance Compose = Compose2
type instance Compose = Compose3
type instance Compose = Compose4

class Partial1 (f :: a -> k) (x :: a) (y :: k) | f x -> y
  
instance Partial1 f x (f x)
class Partial2 (f :: a -> b -> k) (x :: a) (m :: b) (y :: k) | f x m -> y
instance Partial2 f x y (f x y)
class Partial3 (f :: a -> b -> c -> k) (x :: a) (m :: b) (n :: c) (y :: k) | f x m n -> y
instance Partial3 f x y z (f x y z)
class Partial4 (f :: a -> b -> c -> d -> k) (x :: a) (m :: b) (n :: c) (o :: d) (y :: k) | f x m n o -> y
instance Partial4 f x y z a (f x y z a)

type family Partial :: k
type instance Partial = Partial1
type instance Partial = Partial2
type instance Partial = Partial3
type instance Partial = Partial4

class Apply1 (f :: a -> Constraint) (x :: a -> Constraint)
instance (x y, f y) => Apply1 f x
class Apply2 (f :: a -> b -> Constraint) (x :: a -> Constraint) (e :: b)
instance (x y, f y e) => Apply2 f x e
class Apply3 (f :: a -> b -> c -> Constraint) (x :: a -> Constraint) (e :: b) (g :: c)
instance (x y, f y e g) => Apply3 f x e g
class Apply4 (f :: a -> b -> c -> d -> Constraint) (x :: a -> Constraint) (e :: b) (h :: c) (g :: d)
instance (x y, f y e g h) => Apply4 f x e g h

type family (a :: x) $ (b :: y) :: k
type instance a $ b = a b
type instance a $ b = Apply1 a b
type instance a $ b = Apply2 a b
type instance a $ b = Apply3 a b
type instance a $ b = Apply4 a b

class Id (a :: k) (b :: k) | a -> b, b -> a
instance Id a a

class Flip1 (f :: a -> b -> Constraint) (x :: b) (y :: a)
instance f y x => Flip1 f x y
class Flip2 (f :: a -> b -> c -> Constraint) (x :: b) (y :: a) (m :: c)
instance f y x m => Flip2 f x y m
class Flip3 (f :: a -> b -> c -> d -> Constraint) (x :: b) (y :: a) (m :: c) (n :: d)
instance f y x m n => Flip3 f x y m n
class Flip4 (f :: a -> b -> c -> d -> e -> Constraint) (x :: b) (y :: a) (m :: c) (n :: d) (o :: e)
instance f y x m n o => Flip4 f x y m n o

-- >>> T :: (Flip Minus ~ sub, (I 1 `sub` I 2) a) => T a
-- 1
type family Flip :: (x -> y -> k) -> y -> x-> k
type instance Flip = Flip1
type instance Flip = Flip2
type instance Flip = Flip3
type instance Flip = Flip4

class Const1 (a :: k) b (c :: k) | a -> c, c -> a
instance Const1 a b a
class Const2 (a :: k) b c (d :: k) | a -> d, d -> a
instance Const2 a b c a
class Const3 (a :: k) b c d (e :: k) | a -> e, e -> a
instance Const3 a b c d a
class Const4 (a :: k) b c d e (f :: k) | a -> f, f -> a
instance Const4 a b c d e a

type family Const :: k
type instance Const = Const1
type instance Const = Const2
type instance Const = Const3
type instance Const = Const4

-- >>> T :: Until ((<) (I 10)) ((+) (I 2)) (I 1) a => T a
-- 11
-- >>> T :: Until Id (Const True) True a => T a
-- True
class Until (p :: a -> Bool -> Constraint)
            (f :: a -> a -> Constraint)
            (x :: a)
            (y :: a)
instance If (p x) (x ~ y) (f x x', Until p f x' y)
  => Until p f x y

-- ** Lists

instance Shows '[] x ("[]" ': x)
instance (Shows a y z, ShowsTail l ("]" ': x) y) => Shows (a ': l) x ("[" ': z)
class ShowsTail (a :: [k]) (x :: [Symbol]) (y :: [Symbol]) | a x -> y
instance ShowsTail '[] x ("]" ': x)
instance (Shows a y z, ShowsTail l x y) => ShowsTail (a ': l) x ("," ': z)

instance Compare '[] '[] EQ
instance Compare '[] (x ': xs) LT
instance Compare (x ': xs) '[] GT
instance
    (Compare x y o,
     Case o [
      EQ --> Compare xs ys r,
      o --> o ~ r
     ])
    => Compare (x ': xs) (y ': ys) r

instance (Kind x k) => Kind (x ': xs) [k]
-- TODO: k is ambiguous
instance Kind '[] [k]

instance ('[] == '[]) True
instance ((x == y) p, (xs == zs) q, (p && q) o) =>
    ((x ': xs) == (y ': ys)) o

-- >>> T :: Map (Const1 True) '[ '()] a => T a
-- [True]
-- >>> T::T (Map ((+) (I 1)) '[I 2, I 3])
-- [3,4]
class Map (f :: a -> c -> Constraint) (l :: [a]) (j :: [c]) | f l -> j
instance Map f '[] '[]
instance (f x y, Map f xs ys)
    => Map f (x ': xs) (y ': ys)

-- >>> T :: FoldR (+) (I 0) '[I 1, I 2, I 3] l => T l
-- 6
class FoldR (f :: a -> b -> b -> Constraint)
    (nil :: b) (list :: [a]) (ret :: b) | f nil list -> ret
instance Id nil ret => FoldR f nil '[] ret
instance (FoldR f nil xs tail, f x tail ret)
    => FoldR f nil (x ': xs) ret

-- >>> T :: FoldL (+) (I 0) '[I 1, I 2, I 3] l => T l
-- 6
class FoldL (f :: b -> a -> b -> Constraint)
    (accum :: b) (list :: [a]) (ret :: b) | f accum list -> ret
instance FoldL f accum '[] accum
instance (f accum x accum',
          FoldL f accum' xs ret)
    => FoldL f accum (x ': xs) ret                    

class Head (l :: [a]) (x :: a) | l -> x
instance Error "Head: empty list" => Head '[] a
instance Head (x ': xs) x
                      
class Tail (l :: [a]) (x :: [a]) | l -> x
instance Error "Tail: empty list" => Tail '[] a
instance Tail (x ': xs) xs

-- >>> T :: Last '[1,2,3] a => T a
-- 3
class Last (l :: [a]) (x :: a) | l -> x
instance Error "Last: empty list" => Last '[] a
instance a ~ b => Last '[a] b
instance Last (y ': xs) a => Last (x ': y ': xs) a

class Init (l :: [a]) (x :: [a]) | l -> x
instance Error "Init: empty list" => Init '[] a
instance Init '[a] '[]
instance Init (y ': xs) a => Init (x ': y ': xs) (x ': a)

class Null (l :: [a]) (p :: Bool) | l -> p
instance Null '[] True
instance Null (x ': xs) False

class Length (l :: [a]) (i :: Integer) | l -> i
instance Length '[] Zeros
instance (Length xs n, (I 1 + n) i) => Length (x ': xs) i

-- >>> T :: ('[1,2,3] !! I 1) a => T a
-- 2
class ((l :: [a]) !! (n :: Integer)) (x :: a) | l n -> x
instance Error "(!!): index too large" => ('[] !! n) x
instance y ~ x => ((x ': xs) !! Zeros) y
instance (xs !! i) y
    => ((x ': xs) !! One i) y
instance (Drop i xs ys, (ys !! i) y)
    => ((x ': xs) !! Zero i) y

-- >>> T :: (Drop (I 1) '[1,2,3,4] a, Length a b) => T b
-- 3
class Drop (i :: Integer) (l :: [a]) (k :: [a]) | i l -> k
instance a ~ b => Drop Zeros a b
instance Error "Drop: negative count" => Drop Ones a b
instance Drop i '[] '[]
instance (Drop i xs ys, Drop i ys zs) => Drop (One i) (x ': xs) zs
instance (Drop i xs ys, Drop i ys zs) => Drop (Zero i) xs zs

-- >>> T :: ('[1,2,3] ++ '[4,5,6]) l => T l
-- [1,2,3,4,5,6]
class ((a :: [k]) ++ (b :: [k])) (c :: [k]) | a b -> c
instance ('[] ++ b) b
instance (a ++ b) c => ((x ': a) ++ b) (x ': c)

-- >>> T :: Concat '[ '[1,2], '[3,4], '[5,6]] l => T l
-- [1,2,3,4,5,6]
type Concat = FoldR (++) '[]

class ConcatMap (f :: k -> [x] -> Constraint) (a :: [k]) (b :: [x]) | f a -> b
instance (Map f l k, Concat k j) => ConcatMap f l j

-- >>> T :: ScanL (+) (I 0) '[I 1, I 2, I 3, I 4] l => T l
-- [0,1,3,6,10]
class ScanL (f :: a -> b -> a -> Constraint) (x :: a) (l :: [b]) (k :: [a]) | f x l -> k
instance ScanL f x '[] '[x]
instance (f x y z, ScanL f z ys zs) => ScanL f x (y ': ys) (x ': zs)

-- >>> T :: ScanR (+) (I 0) '[I 1, I 2, I 3, I 4] l => T l
-- [10,9,7,4,0]
class ScanR (f :: a -> b -> b -> Constraint) (x :: b) (l :: [a]) (k :: [b]) | f x l -> k
instance ScanR f q '[] '[q]
instance (f x z y, ScanR f q xs (z ': ys)) => ScanR f q (x ': xs) (y ': z ': ys)

class ScanFold1 (c :: a -> b -> [b] -> c -> Constraint) (x :: a) (y :: [b]) (z :: c) | c x y -> z
instance c x y ys z => ScanFold1 c x (y ': ys) z

type ScanL1 = ScanFold1 ScanL
type ScanR1 = ScanFold1 ScanR
type FoldL1 = ScanFold1 FoldL
type FoldR1 = ScanFold1 FoldR

class Replicate (i :: Integer) (a :: k) (l :: [k]) | i a -> l
instance Replicate Zeros a '[]
instance (Replicate (i `F.Minus` I 1) a as, l ~ (a ': as)) => Replicate i a l

-- >>> T :: Take (I 3) '[1,2,3,4,5] l => T l
-- [1,2,3]
class Take (i :: Integer) (a :: [k]) (b :: [k]) | i a -> b
instance Take i '[] '[]
instance (F.If (F.IsZero i) (b ~ '[]) (Take (i `F.Minus` I 1) xs t, b ~ (x ': t))) => Take i (x ': xs) b

class SplitAt (i :: Integer) (a :: [k]) (b :: ([k], [k]))
instance (Take i a x, Drop i a y) => SplitAt i a '(x, y)

-- >>> T :: TakeWhile ((>) (I 3)) '[I 1, I 2, I 3, I 4, I 5] l => T l
-- [1,2]
class TakeWhile (f :: a -> Bool -> Constraint) (x :: [a]) (y :: [a])
instance TakeWhile f '[] '[]
instance If (f x) (TakeWhile f xs zs, ys ~ (x ': zs)) (ys ~ '[]) => TakeWhile f (x ': xs) ys

class DropWhile (f :: a -> Bool -> Constraint) (x :: [a]) (y :: [a])
instance DropWhile f '[] '[]
instance If (f x) (DropWhile f xs ys) (ys ~ (x ': xs)) => DropWhile f (x ': xs) ys

class Span (f :: a -> Bool -> Constraint) (x :: [a]) (y :: ([a], [a]))
instance (TakeWhile f a b, DropWhile f a c) => Span f a '(b, c)

class Break (f :: a -> Bool -> Constraint) (x :: [a]) (y :: ([a], [a]))
instance Break f '[] '( '[], '[])
instance If (f x)
            (y ~ '( '[], x ': xs))
            (Break f xs '(a, b), y ~ '(x ': a, b))
       => Break f (x ': xs) y

type And = FoldR (&&) True
type Or  = FoldR (||) False

-- >>> T :: Any ((==) 1) '[3,2,1] p => T p
-- True
type Any = (Compose1 Or) `Compose2` Partial1 Map
type All = (Compose1 And) `Compose2` Partial1 Map

class Elem (a :: k) (b :: [k]) (p :: Bool) | a b -> p
instance Elem a '[] False
instance If (a == x) (p ~ True) (Elem a xs p) => Elem a (x ': xs) p

-- >>> T :: NotElem 2 '[1,3] p => T p
-- True
type NotElem = (Compose1 Not) `Compose2` Partial1 Elem

type Maximum = FoldL1 Max

-- TODO: minimum zip zip3 zipWith zipWith3 unzip unzip3
-- TODO: filter

-- * Integer

-- >>> T :: Show (I 12) s => T s
-- ["1","2"]
instance Shows Zeros x ("0" ': x)
instance If (i > I 0)
            (ShowsInteger i x y) 
            (Negate i j, ShowsInteger j x y', y ~ ("-" ': y'))
         => Shows (i :: Integer) x y
class ShowsInteger (i :: Integer) (x :: [Symbol]) (y :: [Symbol]) | i x -> y
instance ShowsInteger Zeros x x
instance (QuotRem' i (I 10) q r,
          ShowsInteger q (F.Digit r ': x) y)
         => ShowsInteger i x y

instance (Ones == Ones) True
instance (Zeros == Zeros) True
instance (i == j) p => (One i == One j) p
instance (i == j) p => (Zero i == Zero j) p
instance p ~ False => ((i :: Integer) == j) p

instance FromEnum i (i :: Integer)  
instance ToEnum i (i :: Integer)

instance Kind (a :: Integer) Integer

class ((a :: k) + (b :: k)) (sum :: k) | a b -> sum
instance AddWithCarry False a b sum => (a + b) sum

class AddWithCarry (carry :: Bool) (a :: Integer) (b :: Integer)
      (sum :: Integer) | carry a b -> sum
instance AddWithCarry False Zeros a a
instance AddWithCarry False Ones Zeros Ones
instance AddWithCarry True Ones a a
instance AddWithCarry True Zeros Ones Zeros
instance (F.Add3 carry (IntegerHead a) (IntegerHead b) ~ '(head, carry'),
          IntegerTail a ~ a',
          IntegerTail b ~ b',
          AddWithCarry carry' a' b' tail,
          sum ~ IntegerCons head tail)
    => AddWithCarry carry a b sum
    
class Minus (a :: k) (b :: k) (dif :: k) | a b -> dif
--instance (Negate b nb, (a + nb) dif) => Minus a b (dif :: Integer)
instance (Complement b cb, AddWithCarry True a cb dif)
         => Minus a b (dif :: Integer)

class Negate (a :: k) (b :: k) | a -> b
instance (Complement a b,
          (b + (I 1)) c)
    => Negate a (c :: Integer)
         
-- >>> T :: (I 13 * I 14) a => T a
-- 182
class ((a :: k) * (b :: k)) (prod :: k) | a b -> prod
instance (Zeros * a) Zeros
instance Negate a prod => (Ones * a) prod
instance (One Zeros * a) a
instance ((i * a) b, prod ~ IntegerCons False b) => (Zero i * a) prod
instance ((i * a) b,
          b' ~ IntegerCons False b,
          (a + b') prod)
    => (One i * a) prod

class Signum (a :: k) (b :: k) | a -> b
instance Signum Zeros Zeros
instance Signum i s => Signum (Zero i) s
instance Signum' i s => Signum i s

-- Signum' is never 0
class Signum' (a :: k) (b :: k) | a -> b
instance Signum' Zeros (One Zeros)
instance Signum' Ones Ones
instance Signum' i s => Signum' (Zero i) s
instance Signum' i s => Signum' (One i) s

class Abs (a :: k) (b :: k) | a -> b
instance (Signum a s, 
          Case s [Ones --> Negate a b,
                  Otherwise (a ~ b)])
    => Abs a b

class Subtract (a :: k) (b :: k) (dif :: k) | a b -> dif
instance Minus b a dif => Subtract a b dif

class Even (a :: k) (p :: Bool) | a -> p
instance (p ~ (IntegerHead i)) => Even i p

class Odd (a :: k) (p :: Bool) | a -> p
instance Odd Ones True
instance Odd Zeros False
instance Odd (One i) True
instance Odd (Zero i) False

-- >>> T :: Gcd (I 14) (I 6) a => T a
-- 2
class Gcd (a :: k) (b :: k) (c :: k) | a b -> c
instance Error "Gcd 0 0 is undefined" => Gcd Zeros Zeros c
instance (Abs x x',
          Abs y y',
          Gcd' x' y' z)
    => Gcd x y z
class Gcd' (x :: Integer) (y :: Integer) (z :: Integer) | x y -> z
instance Gcd' x Zeros x
instance (Rem x y r,
          Gcd' y r z)
    => Gcd' x y z

-- TODO: lcm, (^), (^^), 

-- Ord Integer
instance (Minus a b d,
          Signum d s,
          Case s [Ones --> p ~ LT,
                  Zeros --> p ~ EQ,
                  One Zeros --> p ~ GT,
                  Otherwise (Error '("Signum returned", s))])
    => Compare (a :: Integer) b p

-- * Misc functions from the Prelude

class Error a
instance ERROR a => Error a
class ERROR a

class AsKindOf (a :: k) (b :: k) | a -> b, b -> a
instance AsKindOf a b

-- * Bits

class Xor (a :: k) (b :: k) (c :: k) | a b -> c, b c -> c, a c -> b

instance c ~ F.Xor a b => Xor (a :: Bool) b c

instance Xor Zeros a a
instance Complement a b => Xor Ones a b
instance (Xor (IntegerHead a) (IntegerHead b) c,
          Xor (IntegerTail a) (IntegerTail b) d,
          e ~ IntegerCons c d)
    => Xor (a :: Integer) b e
class ((a ::  k) .&. (b :: k)) (c :: k) | a b -> c

instance c ~ (a F..&. b) => (a .&. b) c

instance (Zeros .&. a) Zeros
instance (Ones .&. a) a
instance ((True .&. (IntegerHead b)) c,
          (a .&. (IntegerTail b)) d,
          e ~ IntegerCons c d)
    => ((One a) .&. b) (e :: Integer)
instance ((False .&. (IntegerHead b)) c,
          (a .&. (IntegerTail b)) d,
          e ~ IntegerCons c d)
    => ((Zero a) .&. b) (e :: Integer)

class Complement (a :: k) (b :: k) | a -> b, b -> a

instance Complement True False
instance Complement False True

instance Complement Zeros Ones
instance Complement Ones Zeros
instance (Complement (IntegerHead a) head,
          Complement (IntegerTail a) tail,
          b ~ IntegerCons head tail)
         => Complement a (b :: Integer)

-- * Integral

-- >>> T :: QuotRem (I 11) (I 3) k => T k
-- (3,2)
class QuotRem (a :: k) (b :: k) (c :: (k, k)) | a b -> c
instance Error "Division by zero" => QuotRem (a :: Integer) Zeros b
instance (Abs a a', Abs b b',
          QuotRem' a' b' q r,
          Signum a sa, Signum b sb,
          (sa * r) rem,
          (sa * q) q',
          (sb * q') quot)
    => QuotRem (a :: Integer) b '(quot, rem)

class QuotRem' (a :: Integer) (b :: Integer) (q :: Integer) (r :: Integer)
instance (If (a < b)
             ('(q, r) ~ '(I 0, a))
             ((I 2 * b) b2,
              QuotRem' a b2 q' r',
              (q' * I 2) q'',
              If (r' >= b)
                 ((I 1 + q'') q,
                  (r' `Minus` b) r)
                 (q ~ q'', r' ~ r)))
          => QuotRem' a b q r

-- >>> T :: Rem (I 13) (I 7) a => T a
-- 6
class Rem (a :: k) (b :: k) (c :: k) | a b -> c
instance (QuotRem a b '(q, r)) => Rem a b (r :: Integer)

class Quot (a :: k) (b :: k) (c :: k) | a b -> c
instance (QuotRem a b '(q, r)) => Quot a b (q :: Integer)
         
-- TODO: quot, div, mod, quotRem, divMod, toInteger

-- * Miscellanous

-- | TypeEq

class TypeEq' '() x y b => TypeEq (x :: k) (y :: k) (b :: Bool) | x y -> b
class TypeEq' (q :: ()) (x :: k) (y :: k) (b :: Bool) | q x y -> b
class TypeEq'' (q :: ()) (x :: k) (y :: k) (b :: Bool) | q x y -> b
instance TypeEq' '() x y b => TypeEq x y b
instance b ~ True => TypeEq' '() x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' '() x y False