{-# LANGUAGE
  UndecidableInstances, IncoherentInstances,
  UnicodeSyntax, TypeOperators, ScopedTypeVariables, MultiParamTypeClasses,
  FunctionalDependencies, TypeSynonymInstances, FlexibleInstances, 
  FlexibleContexts #-}

module Guess.Combinator.Lib (module Prelude, module Data.HList, module Guess.Combinator.Lib) where

import Prelude (($), (++), show, Either(..), Maybe(..), Num(..), Show(..), Bool(..))
import Data.HList (HTrue, HFalse, HNil(HNil), HCons(HCons), (:*:), HAppend, HReverse)
import Data.HList.TypeCastGeneric2 (TypeCast)

-- | FunToList +type -typelist
-- Flatten the functions in a given type, in reverse order
-- 
-- For example, FunToList (a -> (b -> c) -> d) [d, [c, [b]], [a]]

class FunToList t tl | t → tl

instance (IsFunction t flag,
          FunToList' flag t tl)
         ⇒ FunToList t tl

class FunToList' a t tl | a t → tl

instance FunToList' HFalse t (t :*: HNil)

instance (FunToList x tlx,
          FunToList y tly,
          HAppend tly (tlx :*: HNil) tl) 
       ⇒ FunToList' HTrue (x → y) tl

-- | ListToFun +typelist -type
-- 
-- Reverse of FunToList

class ListToFun tl t | tl → t

instance ListToFun (t :*: HNil) t

instance (ListToFun tl a,
          ListToFun ((a → r) :*: tls) t)
         ⇒ ListToFun (r :*: (tl :*: tls)) t

-- Misc type-level programming classes and helpers

infixr 2 .*.
a .*. b = HCons a b

class IsFunction a b | a → b
instance TypeCast f HTrue ⇒ IsFunction (x → y) f
instance TypeCast f HFalse ⇒ IsFunction a f

class TypeEq' () x y b ⇒ TypeEq x y b | x y → b
class TypeEq' q x y b | q x y → b
class TypeEq'' q x y b | q x y → b
instance TypeEq' () x y b ⇒ TypeEq x y b
instance TypeCast b HTrue ⇒ TypeEq' () x x b
instance TypeEq'' q x y b ⇒ TypeEq' q x y b
instance TypeEq'' () x y HFalse

data Proxy t = Proxy