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

-- | Guess a value for a combinator
--
-- Based on De-typechecker: converting from a type to a term
-- by <oleg at pobox.com>

module Guess.Combinator (combinator) where

import Guess.Combinator.Lib

-- | Guess a combinator given its type
--
-- Example:
--
-- >>> let f = combinator :: (b -> c) -> (a -> b) -> a -> c
-- >>> f (:[]) ((,) True) 10
-- [(True, 10)]

combinator ∷ GuessCombinator t HNil ⇒ t
combinator = combinatorWith emptyEnv

-- | Tests
test =
((combinator ∷ a → (a → b) → b) 'O' (:"K"), "OK")
.*. (combinator 'O' (:"K") :: String, "OK")
.*. ((combinator ∷ a → (a → b) → b) 1 (+2), 3)
.*. ((combinator ∷ (b → c) → (a → b) → a → c) Just Right True, Just (Right True))
.*. ((combinator ∷ a → b → a) 'a' 'b', 'a')
.*. ((combinator ∷ (t → t1) → t → t2 → t1) Just 1 'c', Just 1)
.*. ((combinator ∷ (b → c) → (a → b) → a → c) (:[]) ((,) True) 10, [(True, 10)])
.*. ((combinator ∷ (((a → b → c) → (a → b) → a → c)→ (t3 → t1 → t2 → t3) → t) → t) (\f g → f (g 1) (:[]) 2), 1)
.*. ((combinator ∷ ((a → b) → c) → (a → b) → c) (\$2) (+3), 5)
.*. (combinator 'a' True ∷ Bool, True)
.*. HNil

-- | A type/value pair
--
-- The list representation of the type is also kept.

newtype TypeToTermT tl t = TypeToTermT t deriving Show

-- | GuessCombinator +type +env
-- Guess a combinator given its type and an environment

class GuessCombinator t env where
combinatorWith ∷ env → t

instance (IsFunction t flag,
GuessWith' flag t env)
⇒ GuessCombinator t env where
combinatorWith = guessWith' (Proxy ∷ Proxy flag)

class GuessWith' flag t env where
guessWith' ∷ (Proxy flag) → env → t

-- | If its a function, add the argument to the environment and guess the result
instance (IsFunction x flagx,
FunToList' flagx x tlx,
IsFunction y flagy,
GuessWith' flagy y ((TypeToTermT tlx x) :*: env))
⇒ GuessWith' HTrue (x → y) env where
guessWith' _ env = \(v ∷ x) →
guessWith' (Proxy ∷ Proxy flagy) (((TypeToTermT v) ∷ TypeToTermT tlx x) .*. env)

-- | If it's not a function, let RResolve find a suitable value
instance (RResolve env ((t :*: HNil) :*: HNil) HNil t)
⇒ GuessWith' HFalse t env where
guessWith' _ env = rresolve env (Proxy ∷ Proxy ((t :*: HNil) :*: HNil)) HNil

-- | RResolve +env +goals +retlist -ret
-- Type-level SLD resolution algorithm
--
-- env: a list of TypeToTermT
-- goals: the tail of a flattened type
-- retlist: a function and arguments, reversed, such as any one of tails [a, b, b -> a -> ret]
-- ret: resulting type/value (a collapsed retlist)

class RResolve env goals tl t | env goals tl → t where
rresolve ∷ env → (Proxy goals) → tl → t

-- | When there are no goals left and the retlist is a singleton, return it

instance RResolve env HNil (t :*: HNil) t where
rresolve _ _ (HCons t HNil) = t

-- | When there are no goals left and the retlist is not a singleton, collapse the retlist

instance RResolve env HNil (t1 :*: tr) (t→r)
⇒ RResolve env HNil (t :*: t1 :*: tr) r where
rresolve g _ (HCons t r) = (rresolve g (Proxy ∷ Proxy HNil) r) t

-- | When the type we want is not a function, look it up in the environment.
-- If we have a function that returns it, save the function and guess its arguments.

instance (RHLookup g env (TypeToTermT (g :*: assum) g'),
HReverse assum assum',
RResolve env assum' (g' :*: HNil) ra,
RResolve env gr (ra :*: pt) t)
⇒ RResolve env ((g :*: HNil) :*: gr) pt t where
rresolve env _ pt = rresolve env (Proxy ∷ Proxy gr) (ra .*. pt)
where
TypeToTermT t1 = rhlookup (Proxy ∷ Proxy g) env
ra ∷ ra = rresolve env (Proxy ∷ Proxy assum') (t1 .*. HNil)

-- | The instance for improper combinators was left as an exercise.
--
-- When we need a function, build the function, add its arguments to the
-- environment and guess the result.

instance (HReverse (gc :*: gcr) revr,
ExtendEnv env revr ra env' f,
RResolve env' ((g :*: HNil) :*: HNil) HNil ra,
RResolve env gr (f :*: pt) t)
⇒ RResolve env ((g :*: gc :*: gcr) :*: gr) pt t where
rresolve (env ∷ env) _ (pt ∷ pt) = rresolve env (Proxy ∷ Proxy gr) (f .*. pt)
where
f ∷ f
f = extendEnv env (Proxy ∷ Proxy revr) \$ \(env' ∷ env') →
rresolve env' (Proxy ∷ Proxy ((g :*: HNil) :*: HNil)) HNil

-- | Extend an environment with the arguments of a function.
--
-- The argument list must be the reverse of the tail of the flattened
-- function type.
--
-- Given a continutation, return a function that builds the environment.
-- For example:
-- extendEnv [] [[a] [b]] k = \a b -> k env'

class ExtendEnv env vs ret env' fun | env vs ret → env' fun where
extendEnv ∷ env → (Proxy vs) → (env' → ret) → fun

instance ExtendEnv env HNil ret env ret where
extendEnv env _ k = k env

instance
(ExtendEnv env rest ret env' fun,
ListToFun pt t)
⇒ ExtendEnv env (pt :*: rest) ret ((TypeToTermT pt t) :*: env') (t → fun)
where
extendEnv env _ f = \(t ∷ t) →
extendEnv env (Proxy ∷ Proxy rest) \$ \env' →
f ((TypeToTermT t ∷ TypeToTermT pt t) .*. env')

-- | Lookup in the `associative' type-indexed list

class RHLookup t l w | t l → w where
rhlookup ∷ (Proxy t) → l → w

instance (TypeEq t t' flag, RHLookup' flag t ((TypeToTermT (t' :*: at) tt') :*: r) w)
⇒ RHLookup t ((TypeToTermT (t' :*: at) tt') :*: r) w where
rhlookup = rhlookup' (Proxy ∷ Proxy flag)

class RHLookup' flag t l w | flag t l → w where
rhlookup' ∷ (Proxy flag) → (Proxy t) → l → w

instance RHLookup' HTrue t ((TypeToTermT (t :*: at) tt) :*: r)
(TypeToTermT (t :*: at) tt) where
rhlookup' _ _ (HCons t _) = t

instance RHLookup t r w ⇒ RHLookup' HFalse t ((TypeToTermT tl' t') :*: r) w where
rhlookup' _ t (HCons _ r) = rhlookup t r

-- | An empty environment.
emptyEnv = HNil

-- | Add a type/value to the environment
consEnv ∷ FunToList t tl ⇒ t → env → TypeToTermT tl t :*: env
consEnv x env = TypeToTermT x .*. env
```