{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Calculus.Lambda.Omega.Explicit where

import Control.Arrow
import Control.Monad
import qualified Data.Char as Char
import Data.Function (on)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes)
import Data.Maybe (fromJust)
import Data.Monoid ((<>))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
import qualified Data.Text.Lazy as TL
import qualified Data.Text.Lazy.Builder as Builder
import Data.Typeable as Typeable
import Data.Bool
import Data.Eq (Eq(..))
import Data.Maybe (Maybe(..), maybe)
import Data.Foldable (Foldable(..))
import Data.Either (Either(..))
import Data.List ((++))
import Data.Monoid (Monoid(..))
import Data.Function (($), (.), id, const, flip)
import Data.String (String)
import Data.Traversable (Traversable(..))
import Data.Ord (Ord(..))
import Control.Applicative (Applicative(..), (<$>))
import Text.Show (Show(..), showParen, showString)
import Prelude (Int, Integer, Num(..), error)
import System.IO (IO)

-- import Debug.Trace

import Calculus.Abstraction.DeBruijn.Generalized

-- * Type 'Term'
-- | 'Term' @var@ forms the main /Abstract Syntax Tree/
-- of the present /explicitely typed/ (aka. /à la Church/) /lambda-calculus/,
-- whose /term constructors/ are:
--
-- * 'TeTy_Var':      for /term variable/ or /type variable/, see 'Abstraction'.
-- * 'TeTy_App':      for /term application/ or /type application/, see 'normalize'.
-- * 'Term_Abst':     for /term abstraction/ (aka. /λ-term/), see 'Abstraction'.
-- * 'Type_Abst':     for /type abstraction/ (aka. /Π-type/, aka. /dependent product/), see 'sort_of_type_abst'.
-- * 'Type_Sort':     for /sort constant/ of a /Pure Type System/ (aka. /PTS/), see 'sort_of_sort'.
-- * 'TeTy_Axiom':    for /custom axiom/, see 'Axiomable'.
--
-- Note that 'Type' and 'Term' share this same data-type
-- (hence the varying prefixes of the Haskell /data constructors/),
-- which avoids duplication of code for their common operations.
--
-- Note that this Haskell type DOES NOT guarantee by itself
-- the /well-formedness/ of the 'Term' (or 'Type'),
-- for instance one can construct such @malformed_type@: @(* *)@:
--
-- @
-- > let star = 'Type_Sort' 'sort_star_mono'
-- > let malformed_type = 'TeTy_App' star star
-- > 'left' 'type_error_msg' '$' 'type_of' 'context' malformed_type
-- Left ('Type_Error_Msg_Not_a_function' … )
-- @
--
-- Though an Haskell type could be crafted to get a stronger guarantee
-- over the /well-formedness/, it is not done here
-- for the following reasons :
--
-- 1. The /well-formedness/ alone is not really useful,
-- it’s the /well-typedness/ which matters,
-- and this depends upon a specific 'Context'.
--
-- 2. Guaranteeing a good combinaison of 'TeTy_App' with respect to 'Term_Abst' (or 'Type_Abst')
-- while using the 'Abstraction' approach could be done:
-- for instance by using @GADTs@ on 'Term'
-- to add an Haskell /type parameter/ @ty@ (aka. /index/)
-- constrained to @(i -> o)@, @i@ or @o@ depending on the /term constructors/,
-- and then by defining Haskell /type classes/
-- replicating: 'Functor', 'Foldable', 'Traversable', 'Monad' and 'Monad_Module_Left',
-- but working on /natural transformations/ (giving /indexed functors/, /indexed monads/, …),
-- however this yields to a significant increase in code complexity,
-- which is not really worth the resulting guarantee
-- (to my mind, here, simplicity has priority
-- over comprehensive automated checking,
-- especially since it’s a research project
-- where I don't fully know all what will be needed
-- and thus appreciate some level of flexibility).
--
-- So, with this actual 'Term' data-type:
-- 'type_of' MUST be used to check the /well-formedness/ along the /well-typedness/
-- of a 'Term' (or equivalently of a 'Type') with respect to a 'Context'.
data Term var
 =   TeTy_Var  var
 |   TeTy_App  (Term var) (Term var)
 |   Term_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Term) var)
 |   Type_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) (Type) var)
 |   Type_Sort Sort
 |   forall ax .
     ( Axiomable (Axiom ax)
     , Typeable ax
     ) => TeTy_Axiom (Axiom ax)
 -- deriving (Eq, Show, Functor, Foldable, Traversable)
-- | 'Eq' instance ignores /bound variables/' 'Var_Name',
-- effectively testing for /α-equivalence/.
instance (Eq var, Show var) => Eq (Term var) where
	TeTy_Var x         == TeTy_Var y         = x   == y
	TeTy_App xf xa     == TeTy_App yf ya     = xf  == yf  && xa == ya
	Term_Abst _ xty xf == Term_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
	Type_Abst _ xty xf == Type_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
	Type_Sort x        == Type_Sort y        = x   == y
	TeTy_Axiom x       == TeTy_Axiom y       = x `axiom_eq` y
	_ == _ = False
deriving instance Show var => Show (Term var)
-- | A 'Functor' instance capturing the notion of /variable renaming/.
deriving instance Functor Term
deriving instance Foldable Term
deriving instance Traversable Term
deriving instance Typeable Term
instance Show1 Term where showsPrec1 = showsPrec
instance Eq1   Term where (==#) = (==)

instance Applicative (Term) where
	pure = TeTy_Var
	(<*>) = ap
-- | A 'Monad' instance capturing the notion of /variable substitution/ with /capture-avoiding/.
instance Monad (Term) where
	return = pure
	Type_Sort        s >>= _  = Type_Sort s
	TeTy_Axiom       a >>= _  = TeTy_Axiom a
	TeTy_Var         v >>= go = go v
	TeTy_App    f    x >>= go = TeTy_App    (f    >>= go) (x  >>= go)
	Term_Abst v f_in f >>= go = Term_Abst v (f_in >>= go) (f >>>= go)
	Type_Abst v f_in f >>= go = Type_Abst v (f_in >>= go) (f >>>= go)
instance Buildable var => Buildable (Term var) where
	build = go False False
		where
		go :: forall v. (Buildable v)
		 => Bool -> Bool
		 -> Term v
		 -> Builder.Builder
		go parenBind parenApp te =
			case te of
			 Type_Sort s -> build s
			 TeTy_Axiom ax -> build ax
			 TeTy_Var v -> build v
			 TeTy_App f x ->
				(if parenApp then "(" else "")
				<> go True False f <> " " <> go True True x
				<> (if parenApp then ")" else "")
			 Term_Abst _ _ _ ->
				(if parenBind then "(" else "")
				<> "λ"{- <> "\\"-} <> go_abst parenBind parenApp te
			 Type_Abst (Suggest x) f_in f_out ->
				(if parenBind then "(" else "")
				<> (if x == ""
					then go True  False f_in
					else "∀" <> "(" <> build x <> ":" <> go False False f_in <> ")" )
				<> " -> "
				<> go False False (abstract_normalize f_out)
				<> (if parenBind then ")" else "")
		go_abst :: forall v. (Buildable v)
		 => Bool -> Bool
		 -> Term v
		 -> Builder.Builder
		go_abst parenBind parenApp te =
			case te of
			 Term_Abst (Suggest x) f_in f ->
				let body = abstract_normalize f in
				case body of
				 Term_Abst _ _ _ ->
					"(" <> go_var_def x <> ":" <> go False False f_in <> ")"
					<> " " <> go_abst parenBind parenApp body
				 _ ->
					"(" <> go_var_def x <> ":" <> go False False f_in <> ")"
					<> " -> "
					<> go False False body
					<> (if parenBind then ")" else "")
			 _ -> go parenBind parenApp te
		go_var_def x = if x == "" then "_" else build x

-- ** Type 'Sort'
-- | Four /PTS/ /sort constants/
-- are formed by combining
-- 'Type_Level' and 'Type_Morphism':
--
-- * @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
-- * @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
-- * @□m@: the 'Sort' to form the 'Type' of a monomorphic 'Type'.
-- * @□p@: the 'Sort' to form the 'Type' of a polymorphic 'Type'.
type Sort = (Type_Level, Type_Morphism)
instance Buildable Sort where
	build x = case x of
	 (sort, morphism) -> build sort <> build morphism

-- | @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
sort_star_mono :: Sort
sort_star_mono = (Type_Level_0, Type_Morphism_Mono)

-- | @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
sort_star_poly :: Sort
sort_star_poly = (Type_Level_0, Type_Morphism_Poly)

-- *** Type 'Type_Level'
data Type_Level
 =   Type_Level_0 -- ^ aka. /@*@ (Star) sort constant/.
 |   Type_Level_1 -- ^ aka. /@□@ (Box)  sort constant/.
 deriving (Eq, Ord, Show)
instance Buildable Type_Level where
	build x = case x of
	 Type_Level_0 -> "*"
	 Type_Level_1 -> "□"

-- *** Type 'Type_Morphism'
data Type_Morphism
 =   Type_Morphism_Mono
 |   Type_Morphism_Poly
 deriving (Eq, Ord, Show)
instance Buildable Type_Morphism where
	build x = case x of
	 Type_Morphism_Mono -> "" -- "m"
	 Type_Morphism_Poly -> "p"

-- | /PTS/ axioms for 'Sort':
--
-- * AXIOM: @⊦ *m : □m@
-- * AXIOM: @⊦ *p : □p@
sort_of_sort :: Sort -> Either Type_Error_Msg Sort
sort_of_sort (Type_Level_0, Type_Morphism_Mono)
 = return (Type_Level_1, Type_Morphism_Mono)
 -- AXIOM: @*m : □m@
 -- The type of MONOMORPHIC types of terms,
 -- is of type: the type of types of MONOMORPHIC types of terms
sort_of_sort (Type_Level_0, Type_Morphism_Poly)
 = return (Type_Level_1, Type_Morphism_Poly)
 -- AXIOM: @*p : □p@
 -- The type of POLYMORPHIC types of terms,
 -- is of type: the type of types of POLYMORPHIC types of terms
sort_of_sort s = Left $ Type_Error_Msg_No_sort_for_sort s

-- * Type 'Form'

-- | A record to keep a same 'Term' (or 'Type')
-- in several forms (and avoid to 'normalize' it multiple times).
data Form var
 =   Form
 {   form_given  :: Term var
 ,   form_normal :: Term var -- ^ 'normalize'-d version of 'form_given'.
 } deriving (Functor, Show)

-- | Return a 'Form' from a given 'Term'.
form :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Form var
form ctx te = Form te (normalize ctx te)

-- | Reduce given 'Term' (or 'Type') to /normal form/ (NF)
-- by recursively performing /β-reduction/ and /η-reduction/.
-- 
-- Note that any well-typed 'Term' (i.e. for which 'type_of' returns a 'Type')
-- is /strongly normalizing/ (i.e. 'normalize' always returns,
-- and its returned 'Term' is unique up to /α-equivalence/).
normalize :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
normalize = go []
	where
	{-
	go_debug :: (Eq var, Ord var, Variable var, Typeable var)
	 => [Term var]
	 -> Context var
	 -> Term var
	 -> Term var
	go_debug args ctx te =
		go args ctx $
		trace ("normalize: "
		 ++ "\n te = " ++ show te
		 ++ "\n args = " ++ show args
		 ) $ te
	-}
	
	go :: (Eq var, Ord var, Variable var, Typeable var)
	 => [Term var]
	 -> Context var
	 -> Term var
	 -> Term var
	go args ctx (TeTy_Var ((form_normal <$>) . context_item_term <=< context_lookup ctx -> Just te))
	 -- NOTE: Replace variable mapped by the context
	 = case args of
		 [] -> te -- NOTE: no need to normalize again
		 _  -> go args ctx te
	go args ctx (TeTy_App f x)
	 -- NOTE: Normalize and collect applied arguments,
	 -- this to normalize an argument only once for all patterns.
	 = go (go [] ctx x : args) ctx f
	go [] ctx (Term_Abst x f_in f)
	 -- NOTE: η-reduce: Term_Abst _ (TeTy_App f (TeTy_Var (Var_Bound _)) ==> f
	 = (Term_Abst x (go [] ctx f_in) ||| id)
		 (abst_eta_reduce ctx f)
	go (x:args) ctx (Term_Abst _ _ f)
	 -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
	 = go args ctx (const x `unabstract` f)
	go args ctx (Type_Abst x f_in f_out)
	 -- NOTE: Recurse in Type_Abst fields
	 = term_apps (Type_Abst x (go [] ctx f_in) (go_scope ctx f_out)) args
	go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
	 -- NOTE: Normalize axiom
	 = go r_args ctx r_te
	go args _ctx te
	 -- NOTE: Reapply remaining arguments, normalized
	 = term_apps te args
	
	abst_eta_reduce
	 :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
	 => Context var
	 -> Abstraction bound (Term) var
	 -> Either (Abstraction bound (Term) var) -- could not η-reduce
	           (Term var)                     -- could     η-reduce
	abst_eta_reduce ctx =
		(\abst_body ->
			let new_ctx = context_push_nothing ctx in
			case go [] new_ctx abst_body of
			 te@(TeTy_App t (TeTy_Var (Var_Bound _{-Term_Abst's variable-}))) ->
				traverse (\var ->
					case var of
					 Var_Free v -> Right v
						 -- NOTE: decrement the DeBruijn indexing by one
						 -- to reflect the removal of the Term_Abst.
					 Var_Bound _ -> Left $ abstract_generalize te
						 -- NOTE: cannot η-reduce because Term_Abst's variable
						 -- is also used within t.
				 ) t
			 te -> Left $ abstract_generalize te
		 ) .
		abstract_normalize
	
	go_scope
	 :: (Eq var, Eq bound, Ord var, Ord bound, Variable var, Variable bound, Typeable var, Typeable bound)
	 => Context var
	 -> Abstraction bound (Term) var
	 -> Abstraction bound (Term) var
	go_scope ctx =
		abstract_generalize .
		go [] (context_push_nothing ctx) .
		abstract_normalize

-- | Reduce given 'Term' to /Weak Head Normal Form/ (WHNF).
--
-- __Ressources:__
--
-- * https://wiki.haskell.org/Weak_head_normal_form
whnf :: (Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var
whnf = go []
	where
	go :: (Ord var, Variable var, Typeable var) => [Term var] -> Context var -> Term var -> Term var
	go args ctx (TeTy_Var ((form_given <$>) .
	 context_item_term <=< context_lookup ctx
	 -> Just te))
	 -- NOTE: Replace any variable mapped by the context
	 = go args ctx te
	go args ctx (TeTy_App f a)
	 -- NOTE: Collect applied arguments
	 = go (a:args) ctx f
	go (x:args) ctx (Term_Abst _ _ f)
	 -- NOTE: β-reduce: TeTy_App (Term_Abst _ _ f) x ==> f x
	 = go args ctx (const x `unabstract` f)
	go args ctx (TeTy_Axiom (flip (axiom_normalize ctx) args -> Just (r_te, r_args)))
	 -- NOTE: Normalize axiom
	 -- TODO: maybe introduce an 'axiom_whnf' instead of 'axiom_normalize'
	 = go r_args ctx r_te
	go args _ctx te
	 -- NOTE: Reapply remaining arguments, normalized
	 = term_apps te args

-- | Apply multiple 'Term's to a 'Term',
-- useful to reconstruct a 'Term' while normalizing (see 'normalize' or 'whnf').
term_apps :: Term var -> [Term var] -> Term var
term_apps = foldl TeTy_App

-- | /α-equivalence relation/, synonym of @(==)@.
--
-- Return 'True' iif. both given 'Term's are the same,
-- up to renaming the /bound variables/ it contains (see instance 'Eq' of 'Suggest').
alpha_equiv :: (Eq var, Show var) => Term var -> Term var -> Bool
alpha_equiv = (==)

-- | /αβη-equivalence relation/.
equiv :: (Eq var, Ord var, Variable var, Typeable var) => Context var -> Term var -> Term var -> Bool
-- equiv ctx = (==) `on` (normalize ctx)
equiv ctx = (==) `on` normalize ctx

-- * Type 'Type'

-- | 'Type' and 'Term' share the same data-type.
type Type = Term

-- | Construct the 'Type' of the given 'Term',
-- effectively checking for the /well-formedness/
-- and /well-typedness/ of a 'Term' (or 'Type').
--
-- Note that a 'Type' is always to be considered
-- according to a given 'Context':
-- 'type_of' applied to the same 'Term'
-- but on different 'Context's
-- may return a different 'Type' or 'Type_Error'.
type_of
 :: (Eq var, Ord var, Variable var, Typeable var)
 => Context var
 -> Term var
 -> Either Type_Error (Type var)
type_of ctx term =
	case term of
	 Type_Sort s -> (err +++ Type_Sort) $ sort_of_sort s
	 TeTy_Var v ->
		case form_normal
		 .   context_item_type
		 <$> context_lookup ctx v of
		 Just ty -> return ty
		 Nothing -> Left $ err $ Type_Error_Msg_Unbound_variable v
	 TeTy_Axiom ax ->
		return $ axiom_type_of ctx ax
	 TeTy_App f x -> do
		f_ty <- whnf ctx <$> type_of ctx f
		(f_in, f_out) <-
			case f_ty of
			 Type_Abst _ i o -> return (i, o)
			 _ -> Left $ err $ Type_Error_Msg_Not_a_function f f_ty
		x_ty <- type_of ctx x
		case equiv ctx x_ty f_in of
		 True  -> return $ const x `unabstract` f_out
		 False -> Left $ err $ Type_Error_Msg_Function_argument_mismatch f_in x_ty
	 Term_Abst (Suggest x) f_in f -> do
		_ <- type_of ctx f_in
		let new_ctx =
			if x == ""
			then context_push_nothing ctx
			else context_push_type ctx (Suggest x) f_in
		f_out <- type_of new_ctx (abstract_normalize f)
		let abst_ty = Type_Abst (Suggest x) f_in (abstract_generalize f_out)
		_ <- type_of ctx abst_ty
		return abst_ty
	 Type_Abst (Suggest x) f_in f -> do
		f_in_ty <- type_of ctx f_in
		f_in_so <- case whnf ctx f_in_ty of
		 Type_Sort s -> return s
		 f_in_ty_whnf -> Left $ err $ Type_Error_Msg_Invalid_input_type f_in_ty_whnf
		let new_ctx =
			if x == ""
			then context_push_nothing ctx
			else context_push_type ctx (Suggest x) f_in
		f_out_ty <- type_of new_ctx (abstract_normalize f)
		f_out_so <- case whnf new_ctx f_out_ty of
		 Type_Sort s -> return s
		 f_out_ty_whnf -> Left $ Type_Error ctx term $
			Type_Error_Msg_Invalid_output_type f_out_ty_whnf (x, f_out_ty_whnf)
		(err +++ Type_Sort) $
			sort_of_type_abst f_in_so f_out_so
	where
	err = Type_Error ctx term

-- | Check that the given 'Term' has the given 'Type'.
check
 :: (Eq var, Ord var, Variable var, Typeable var)
 => Context var
 -> Type var
 -> Term var
 -> Either (Type_Error) ()
check ctx expect_ty te =
	type_of ctx te >>= \actual_ty ->
		if equiv ctx expect_ty actual_ty
		then Right ()
		else Left $ Type_Error
			 { type_error_ctx  = ctx
			 , type_error_term = te
			 , type_error_msg  = Type_Error_Msg_Type_mismatch expect_ty actual_ty (normalize ctx expect_ty) (normalize ctx actual_ty)
			 }

-- | Check that a 'Term' is closed, i.e. has no /unbound variables/.
close :: Term Var_Name -> Either Type_Error (Term ())
close te =
	traverse go te
	where
		go var = Left $
			Type_Error context te $
			Type_Error_Msg_Unbound_variable var

-- | Return the /unbound variables/ of given 'Term'.
unbound_vars :: Ord var => Term var -> Map var ()
unbound_vars = foldr (flip Map.insert ()) mempty

-- | /Dependent product/ rules: @s ↝ t : u@, i.e.
--   "abstracting something of type @s@ out of something of type @t@ gives something of type @u@".
--
-- Given two 'Sort': @s@ and @t@, return a 'Sort': @u@,
-- when ('Type_Abst' @s@ @t@) is ruled legal
-- and has 'Type': 'Type_Sort' ('Sort' @u@).
--
-- The usual /PTS/ rules for /λω/
-- (or equivalently /Type Assignment Systems/ (TAS) rules for /System Fω/)
-- are used here:
--
-- * RULE: @⊦ * ↝ * : *@, aka. /simple types/:
--   "abstracting a term out of a term is valid and gives a term",
--   as in /PTS λ→/ or /TAS F1/.
-- * RULE: @⊦ □ ↝ * : *@, aka. /parametric polymorphism/:
--   "abstracting a type out of a term is valid and gives a term",
--   as in /PTS λ2/ or /TAS F2/ (aka. /System F/).
-- * RULE: @⊦ □ ↝ □ : □@, aka. /constructors of types/:
--   "abstracting a type out of a type is valid and gives a type",
--   as in /PTS λω/ or /TAS Fω/.
--
-- Note that the fourth usual rule is not ruled valid here:
--
-- * RULE: @⊦ * ↝ □ : □@, aka. /dependent types/:
--   "abstracting a term out of a type is valid and gives a type",
--   as in /PTS λPω/ or /TAS DFω/ (aka. /Calculus of constructions/).
--
-- However, to contain /impredicativity/ (see 'Axiom_MonoPoly')
-- the above /sort constants/ are split in two,
-- and the above rules adapted
-- to segregate between /monomorphic types/ (aka. /monotypes/)
-- and /polymorphic types/ (aka. /polytypes/):
--
-- * RULE: @⊦ *m ↝ *m : *m@, i.e. /simple types/, without /parametric polymorphism/.
-- * RULE: @⊦ *m ↝ *p : *p@, i.e. /simple types/, preserving /parametric polymorphism/ capture.
--
-- * RULE: @⊦ *p ↝ *m : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
-- * RULE: @⊦ *p ↝ *p : *p@, i.e. /higher-rank polymorphism/, preserving /parametric polymorphism/ capture.
--
-- * RULE: @⊦ □m ↝ *m : *p@, i.e. /parametric polymorphism/, captured within @*p@ ('sort_star_poly').
-- * RULE: @⊦ □m ↝ *p : *p@, i.e. /parametric polymorphism/, preserving capture.
--
-- * RULE: @⊦ □m ↝ □m : □m@, i.e. /constructors of types/, without /parametric polymorphism/.
-- * RULE: @⊦ □m ↝ □p : □p@, i.e. /constructors of types/, preserving /parametric polymorphism/ capture.
--
-- Note that what is important here is
-- that there is no rule of the form: @⊦ □p ↝ _ : _@,
-- which forbids abstracting a /polymorphic type/ out of anything,
-- in particular the type @*p -> *m@ is forbidden,
-- though 'Axiom_MonoPoly'
-- is given to make it possible within it.
--
-- __Ressources:__
--
-- * /Henk: a typed intermediate language/,
--   Simon Peyton Jones, Erik Meijer, 20 May 1997,
--   https://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz
sort_of_type_abst
 :: Sort
 -> Sort
 -> Either Type_Error_Msg Sort

-- Simple types
sort_of_type_abst
          (Type_Level_0, Type_Morphism_Mono)
          (Type_Level_0, m)
 = return (Type_Level_0, m)
 -- RULE: *m ↝ *m : *m
 -- RULE: *m ↝ *p : *p
 -- abstracting: a MONOMORPHIC term
 -- out of     : a MONOMORPHIC (resp. POLYMORPHIC) term
 -- forms      : a MONOMORPHIC (resp. POLYMORPHIC) term

-- Higher-rank
sort_of_type_abst
          (Type_Level_0, Type_Morphism_Poly)
          (Type_Level_0, _)
 = return (Type_Level_0, Type_Morphism_Poly)
 -- RULE: *p ↝ *m : *p
 -- RULE: *p ↝ *p : *p
 -- abstracting: a POLYMORPHIC term
 -- out of     : a             term
 -- forms      : a POLYMORPHIC term

-- Polymorphism
sort_of_type_abst
          (Type_Level_1, Type_Morphism_Mono)
          (Type_Level_0, _)
 = return (Type_Level_0, Type_Morphism_Poly)
 -- RULE: □m ↝ *m : *p
 -- RULE: □m ↝ *p : *p
 -- abstracting: a MONOMORPHIC type of a term
 -- out of     : a             term
 -- forms      : a POLYMORPHIC term

-- Type constructors
sort_of_type_abst
          (Type_Level_1, Type_Morphism_Mono)
          (Type_Level_1, m)
 = return (Type_Level_1, m)
 -- RULE: □m ↝ □m : □m
 -- RULE: □m ↝ □p : □p
 -- abstracting: a MONOMORPHIC type of a term
 -- out of     : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
 -- forms      : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
 --
 -- NOTE: □m ↝ □p : □p is useful for instance to build List_:
 -- let List_ : (A:*m) -> *p = \(A:*m) -> (R:*m) -> (A -> R -> R) -> R -> R
 -- let List  : (A:*m) -> *m = \(A:*m) -> Monotype (List_ A)

-- Dependent types

{-
sort_of_type_abst
          (Type_Level_0, Type_Morphism_Mono)
          (Type_Level_1, m)
 = return (Type_Level_1, m)
 -- RULE: *m ↝ □m : □m
 -- RULE: *m ↝ □p : □p
 -- abstracting: a MONOMORPHIC term
 -- out of     : a MONOMORPHIC (resp. POLYMORPHIC) type of a term
 -- forms      : a MONOMORPHIC (resp. POLYMORPHIC) type of a term

sort_of_type_abst
 (Type_Level_0, Type_Morphism_Poly)
 (Type_Level_1, _)
 = return (Type_Level_1, Type_Morphism_Poly)
 -- RULE: *p ↝ □m : □p
 -- RULE: *p ↝ □p : □p
 -- abstracting: a POLYMORPHIC term
 -- out of     : a             type of a term
 -- forms      : a POLYMORPHIC type of a term
-}

sort_of_type_abst
 s@(Type_Level_0, _)
 t@(Type_Level_1, _)
 = Left $ Type_Error_Msg_Illegal_type_abstraction s t
 -- RULE: * ↝ □ : Illegal
 -- abstracting: a term
 -- out of     : a type of a term
 -- is illegal

-- No impredicativity (only allowed through 'Axiom_MonoPoly')
sort_of_type_abst
 s@(Type_Level_1, Type_Morphism_Poly)
 t@(_, _)
 = Left $ Type_Error_Msg_Illegal_type_abstraction s t
 -- RULE: □p ↝ _ : Illegal
 -- abstracting: a POLYMORPHIC type of a term
 -- out of     : anything
 -- is illegal

-- ** Type 'Type_Error'
data Type_Error
 = forall var. (Ord var, Show var, Buildable var)
 =>  Type_Error
 {   type_error_ctx  :: Context var
 ,   type_error_term :: Term var
 ,   type_error_msg  :: Type_Error_Msg
 }
deriving instance Show Type_Error
instance Buildable Type_Error where
	build (Type_Error ctx te msg) =
		"Error: Type_Error"
		 <> "\n " <> build msg
		 <> "\n Term:" <> " " <> build te
		 <> (
			let vars =
				Map.keys $
				Map.intersection
				 (unbound_vars te)
				 (Map.fromList $ (, ()) <$> context_vars ctx) in
			case vars of
			 [] -> "\n"
			 _ -> "\n Context:\n" <> build ctx{context_vars=vars}
		 )

-- ** Type 'Type_Error_Msg'
data Type_Error_Msg
 =   Type_Error_Msg_No_sort_for_sort Sort
 |   Type_Error_Msg_Illegal_type_abstraction Sort Sort
 |   forall var. Variable var => Type_Error_Msg_Invalid_input_type  (Type var)
 |   forall var. Variable var => Type_Error_Msg_Invalid_output_type (Type var) (Var_Name, Type var)
 |   forall var. Variable var => Type_Error_Msg_Not_a_function (Term var) (Type var)
 |   forall var. Variable var => Type_Error_Msg_Function_argument_mismatch (Type var) (Type var)
 |   forall var. Variable var => Type_Error_Msg_Unbound_variable var
 |   forall var. Variable var => Type_Error_Msg_Unbound_axiom var
 |   forall var. Variable var => Type_Error_Msg_Type_mismatch (Type var) (Type var) (Type var) (Type var)
deriving instance Show Type_Error_Msg
instance Buildable Type_Error_Msg where
	build msg =
		case msg of
		 Type_Error_Msg_No_sort_for_sort x ->
			"No_sort_for_sort: "
			 <> build x
		 Type_Error_Msg_Illegal_type_abstraction x y ->
			"Illegal_type_abstraction: "
			 <> build x <> " -> " <> build y
		 Type_Error_Msg_Invalid_input_type ty ->
			"Invalid_input_type: "
			 <> build ty
		 Type_Error_Msg_Invalid_output_type f_out (x, f_in) ->
			"Invalid_output_type: "
			 <> build f_out <> "\n"
			 <> " Input binding: "
			 <> "(" <> build x <> " : " <> build f_in <> ")"
		 Type_Error_Msg_Not_a_function f f_ty ->
			"Not_a_function: "
			 <> build f
			 <> " : "
			 <> build f_ty
		 Type_Error_Msg_Function_argument_mismatch f_in x_ty ->
			"Function_argument_mismatch: \n"
			 <> " Function domain: " <> build f_in <> "\n"
			 <> " Argument type:   " <> build x_ty
		 Type_Error_Msg_Unbound_variable var ->
			"Unbound_variable: "
			 <> build var
		 Type_Error_Msg_Unbound_axiom var ->
			"Unbound_axiom: "
			 <> build var
		 Type_Error_Msg_Type_mismatch x y nx ny ->
			"Type_mismatch: \n"
			 <> " Expected type: " <> build x <> " == " <> build nx <> "\n"
			 <> " Actual   type: " <> build y <> " == " <> build ny

-- * Type 'Context'

-- | Map variables of type @var@
-- to their 'Type' and maybe also to their 'Term',
-- both in 'form_given' and 'form_normal'.
data Context var
 =   Context
 {   context_vars   :: [var]
  -- ^ used to dump the 'Context'
 ,   context_lookup :: var -> Maybe (Context_Item var)
  -- ^ used to query the 'Context'
 ,   context_lift   :: Typeable var => Var_Name -> var
  -- ^ used to promote a ('Term' 'Var_Name') to ('Term' @var@)
 ,   context_unlift :: Typeable var => var -> Var_Name
  -- ^ used to unpromote ('Term' @var@) to ('Term' 'Var_Name')
 }
data Context_Item var
 =   Context_Item
 {   context_item_term :: Maybe (Form var)
 ,   context_item_type :: Form var
 } deriving (Functor, Show)

instance Show var => Show (Context var) where
	showsPrec n ctx@Context{context_vars=vars} =
		showParen (n > 10) $
		showString "Context " .
		showsPrec n ((\k ->
			(k, fromJust $ context_item_type
			 <$> context_lookup ctx k))
		 <$> vars) .
		showString " " .
		showsPrec n (catMaybes $ (\k ->
			(k,) . form_given <$>
			(context_item_term =<< context_lookup ctx k))
		 <$> vars)
instance Buildable var => Buildable (Context var) where
	build ctx@Context{context_vars=vars} =
		foldMap (\var ->
			"  " <> build var
			 <> maybe mempty (\ty -> " : " <> build (form_given ty))
				 (context_item_type <$> context_lookup ctx var)
			 {-
			 <> maybe mempty (\te -> " = " <> build (form_given te))
				 (context_item_term =<< context_lookup ctx var)
			 -}
			 <> "\n"
		 ) vars

context :: Context Var_Name
context = Context [] (const Nothing) id id

context_apply :: Context var -> Term var -> Term var
context_apply ctx te =
	te >>= \var ->
		maybe (TeTy_Var var) id $ form_normal <$>
		(context_item_term =<< context_lookup ctx var)

context_push_type
 :: (Eq var, Ord var, Variable var, Typeable var)
 => Context var
 -> bound
 -> Type var
 -> Context (Var bound var)
context_push_type
 ctx@(Context keys lookup var_lift var_unlift)
 bound ty =
	Context
	 { context_vars =
		Var_Bound bound :
		Var_Free `fmap` keys
	 , context_lookup = \var ->
		(Var_Free `fmap`) `fmap`
			case var of
			 Var_Bound _ ->
				Just $ Context_Item
				 { context_item_term = Nothing
				 , context_item_type = form ctx ty
				 }
			 Var_Free v -> lookup v
	 , context_lift = Var_Free . var_lift
	 , context_unlift = \var ->
		case var of
		 Var_Bound _ -> error "context_push_type: context_unlift"
		 Var_Free v  -> var_unlift v
	 }

context_push_nothing
 :: (Show bound, Buildable (Context var), Typeable var, Typeable bound)
 => Context var
 -> Context (Var bound var)
context_push_nothing
 (Context keys lookup var_lift var_unlift) =
	Context
	 { context_vars = Var_Free `fmap` keys
	 , context_lookup = \var ->
		(Var_Free `fmap`) `fmap`
			case var of
			 Var_Bound _ -> Nothing
			 Var_Free v  -> lookup v
	 , context_lift = Var_Free . var_lift
	 , context_unlift = \var ->
		case var of
		 -- DEBUG: Var_Bound (cast -> Just (Suggest b)) -> b
		 -- DEBUG: Var_Bound (cast -> Just b) -> b
		 Var_Bound b -> error $ "context_push_nothing: context_unlift: " ++ show b
		 Var_Free v  -> var_unlift v
	 }

context_from_env :: Env -> Context Var_Name
context_from_env env =
	Context
	 { context_vars   = Map.keys env
	 , context_lookup = \var ->
		(\item -> Context_Item
		 { context_item_term = Just $ env_item_term item
		 , context_item_type =        env_item_type item
		 }) <$> env_lookup env var
	 , context_lift   = id
	 , context_unlift = id
	 }

context_relift :: forall from_var to_var.
 ( Typeable from_var
 , Typeable to_var )
 => Context from_var
 -> Type    from_var
 -> Context to_var
 -> Type    to_var
context_relift from_ctx ty to_ctx =
	( context_lift to_ctx
	. context_unlift from_ctx
	) <$> ty

{-
context_from_list :: Eq var => [(var, Type var)] -> Context var
context_from_list l =
	Context
	 { context_vars   = fst <$> l
	 , context_lookup_type = \var -> List.lookup var l
	 }

-- | Return /free term variables/ of an 'Abstraction'-ed 'Term'.
ftv
 :: Abstraction bound (Term) var
 -> Term (Var bound var)
ftv = abstract_normalize
-}

-- * Type 'Env'
type Env
 = Map Var_Name Env_Item
data Env_Item
 =   Env_Item
 {   env_item_term :: Form Var_Name
 ,   env_item_type :: Form Var_Name
 }
env_item
 :: Context Var_Name
 -> Term Var_Name
 -> Type Var_Name
 -> Env_Item
env_item ctx te ty =
	Env_Item
	 { env_item_term = form ctx te
	 , env_item_type = form ctx ty
	 }

env_lookup :: Env -> Var_Name -> Maybe (Env_Item)
env_lookup env var = Map.lookup var env

env_insert :: Var_Name -> Term Var_Name -> Type Var_Name -> Env -> Env
env_insert var te ty env =
	let ctx = context_from_env env in
	Map.insert var (env_item ctx te ty) env

-- * Type 'Axiom'

data family Axiom r
-- deriving instance Typeable Axiom

axiom_cast :: (Typeable a, Typeable b) => Axiom a -> Maybe (Axiom b)
axiom_cast = cast

-- ** Type 'Axioms'
-- | 'Axioms' are made of 'Axiom's injected in regular 'Env_Item's,
-- see 'env_item_from_axiom'.
type Axioms = Env

env_item_from_axiom
 :: ( Axiomable (Axiom ax)
    , Typeable ax )
 => Context Var_Name -> Axiom ax -> Env_Item
env_item_from_axiom ctx ax =
	Env_Item
	 { env_item_term = form ctx $ TeTy_Axiom ax
	 , env_item_type = form ctx $ axiom_type_of ctx ax
	 }

-- ** Class 'Axiomable'

-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Type_Of ax where
-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Normalize ax where
-- class (Eq ax, Show ax, Buildable ax, Typeable ax) => Axiomable_Eq ax where

-- | Instances of this class are 'Axiom's injectable in 'TeTy_Axiom', that is:
--
-- * they have a 'Type', given by 'axiom_type_of',
-- * and they can perform an optional reduction
--   within 'normalize' or 'whnf', given by 'axiom_normalize'.
class
 ( Eq ax, Show ax, Buildable ax, Typeable ax
 -- , Axiomable_Type_Of ax
 -- , Axiomable_Normalize ax
 -- , Axiomable_Eq ax
 ) => Axiomable ax where
	axiom_type_of
	 :: forall var. Typeable var
	 => Context var -> ax -> Type var
	 -- ^ Return the 'Type' of the given 'Axiomable' instance.
	axiom_normalize
	 :: forall var. (Typeable var, Ord var, Variable var)
	 => Context var -> ax -> [Term var] -> Maybe (Term var, [Term var])
	 -- ^ Custom-'normalize': given a typing 'Context',
	 -- an 'Axiomable' instance
	 -- and a list of arguments, return:
	 --
	 -- * 'Nothing': if the axiom performs no reduction,
	 -- * 'Just': with the reducted 'Term' and the arguments not used by the reduction.
	 --
	 -- Default: @\\_ctx _ax _args -> Nothing@
	axiom_normalize _ctx _ax _args = Nothing
	axiom_eq :: ax -> (forall ax'. Axiomable ax' => ax' -> Bool)
	 -- ^ Custom-bipolymorphic-@(==)@:
	 -- given an 'Axiomable' instance
	 -- return a function to test if any
	 -- other 'Axiomable' instance
	 -- is equal to the first instance given.
	 --
	 -- Default: @maybe False (x ==) (cast y)@
	axiom_eq x y = maybe False (x ==) (cast y)

-- ** Class 'Axiom_Type'

-- | A class to embed an Haskell-type within an 'Axiom'.
class Axiom_Type h where
	axiom_type :: Axiom h
	 -- ^ Construct (implicitely) an Haskell-term representing
	 -- the Haskell-type @h@.
	axiom_Type :: Axiom h -> Type Var_Name
	 -- ^ Return a 'Type' representing the Haskell-type @h@,
	 -- given through its representation as an Haskell-term
	 -- (which is an 'Axiom' and thus has itself a 'Type',
	 -- given by its 'axiom_type_of').

axiom_term
 :: (Axiom_Type h, Typeable h)
 => h -> Axiom (Axiom_Term h)
axiom_term (x::h) =
	Axiom_Term x $ \ctx ->
		context_lift ctx <$> axiom_Type (axiom_type::Axiom h)

-- ** Type 'Axiom_Type_Assume'
-- | An instance to use 'Type' as an 'Axiom'.
data Axiom_Type_Assume
newtype instance Axiom (Axiom_Type_Assume)
 =               Axiom_Type_Assume (Type Var_Name)
 deriving (Eq, Show)
instance Buildable (Axiom Axiom_Type_Assume) where
	build (Axiom_Type_Assume ty) = "(_:" <> build ty <> ")"
instance Axiomable (Axiom Axiom_Type_Assume) where
	axiom_type_of ctx (Axiom_Type_Assume ty) =
		context_lift ctx <$> ty

-- ** Type 'Axiom_MonoPoly'
-- | Non-'Sort' constants for /boxed parametric polymorphism/.
--
-- Used to embed /polymorphic types/ into first-class /monomorphic types/
-- via explicit injection ('Axiom_Term_MonoPoly_Box') and projection ('Axiom_Term_MonoPoly_UnBox') functions.
--
-- Special treatment of 'Axiom_MonoPoly' constructors is done in 'normalize' and 'whnf'
-- to remove adjacent pairs of 'Axiom_Term_MonoPoly_Box' / 'Axiom_Term_MonoPoly_UnBox'
-- or 'Axiom_Term_MonoPoly_UnBox' / 'Axiom_Term_MonoPoly_Box'.
--
-- __Ressources:__
--
-- * /Recasting MLF/, Didier Le Botlan, Didier Rémy, June 2009,
--   https://hal.inria.fr/inria-00156628
data Axiom_MonoPoly
data instance Axiom Axiom_MonoPoly
 =   Axiom_Type_MonoPoly
 |   Axiom_Term_MonoPoly_Box
 |   Axiom_Term_MonoPoly_UnBox
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Axiom_MonoPoly) where
	build ax = case ax of
	 Axiom_Type_MonoPoly       -> "Monotype"
	 Axiom_Term_MonoPoly_Box   -> "monotype"
	 Axiom_Term_MonoPoly_UnBox -> "polytype"
instance Axiomable (Axiom Axiom_MonoPoly) where
	axiom_type_of ctx ax =
		case ax of
		 Axiom_Type_MonoPoly ->
			 -- Monotype : *p -> *m
			Type_Abst "" (Type_Sort sort_star_poly) $
			(const Nothing `abstract`) $
			Type_Sort sort_star_mono
		 Axiom_Term_MonoPoly_Box ->
			 -- monotype : (Polytype : *p) -> Polytype -> Monotype Polytype
			(context_lift ctx <$>) $
			Type_Abst "Polytype" (Type_Sort sort_star_poly) $
			(("Polytype" =?) `abstract`) $
			Type_Abst "" (TeTy_Var "Polytype") $
			(("" =?) `abstract`) $
			TeTy_App
			 (TeTy_Axiom $ Axiom_Type_MonoPoly)
			 (TeTy_Var "Polytype")
		 Axiom_Term_MonoPoly_UnBox ->
			 -- polytype : (Polytype : *p) -> Monotype Polytype -> Polytype
			(context_lift ctx <$>) $
			Type_Abst "Polytype" (Type_Sort sort_star_poly) $
			(("Polytype" =?) `abstract`) $
			Type_Abst ""
			 (TeTy_App
				 (TeTy_Axiom $ Axiom_Type_MonoPoly)
				 (TeTy_Var "Polytype")) $
			 (("" =?) `abstract`) $
			TeTy_Var "Polytype"
	axiom_normalize _ctx
	 Axiom_Term_MonoPoly_UnBox
	 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_Box)) _ty') te:args)
	 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_UnBox / Axiom_Term_MonoPoly_Box
	 = Just (te, args)
	axiom_normalize _ctx
	 Axiom_Term_MonoPoly_Box
	 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_UnBox)) _ty') te:args)
	 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_Box / Axiom_Term_MonoPoly_UnBox
	 = Just (te, args)
	axiom_normalize _ctx _ax _args = Nothing

-- | /PTS/ axioms for 'Axiom_MonoPoly':
--
-- * AXIOM: @⊦ Monotype : *p -> *m@
-- * AXIOM: @⊦ monotype : (Polytype : *p) -> Polytype -> Monotype Polytype@
-- * AXIOM: @⊦ polytype : (Polytype : *p) -> Monotype Polytype -> Polytype@
axioms_monopoly :: Axioms
axioms_monopoly =
	Map.fromList $
	[ ("Monotype", item Axiom_Type_MonoPoly)
	, ("monotype", item Axiom_Term_MonoPoly_Box)
	, ("polytype", item Axiom_Term_MonoPoly_UnBox)
	]
	where
	item = env_item_from_axiom ctx
	ctx = context_from_env mempty

-- ** Type 'Axiom_Term'

-- | Embed an Haskell-term of Haskell-type @h@ within an 'Axiom'
data Axiom_Term h
data instance Axiom (Axiom_Term h)
 = Typeable h
 => Axiom_Term h
               (forall var. Typeable var => Context var -> Type var)
 deriving (Typeable)

-- Instance 'Axiom' 'Integer'
data instance Axiom Integer
 = Axiom_Type_Integer
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Integer) where
	build Axiom_Type_Integer = "Int"
instance Axiomable (Axiom Integer) where
	axiom_type_of _ctx Axiom_Type_Integer =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type Integer where
	axiom_type = Axiom_Type_Integer
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term Integer)) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term Integer)) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term Integer)) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term Integer)) where
	build (Axiom_Term i _ty) = build i
instance Axiomable (Axiom (Axiom_Term Integer)) where
	axiom_type_of _ctx (Axiom_Term _ _ty) =
		TeTy_Axiom Axiom_Type_Integer

-- Instance 'Axiom' '()'
data instance Axiom ()
 = Axiom_Type_Unit
 deriving (Eq, Ord, Show)
instance Buildable (Axiom ()) where
	build (Axiom_Type_Unit) = "()"
instance Axiomable (Axiom ()) where
	axiom_type_of _ctx Axiom_Type_Unit =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type () where
	axiom_type = Axiom_Type_Unit
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term ())) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term ())) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term ())) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term ())) where
	build (Axiom_Term _te _ty) = "()"
instance Axiomable (Axiom (Axiom_Term ())) where
	axiom_type_of _ctx (Axiom_Term _te _ty) =
		TeTy_Axiom Axiom_Type_Unit

-- Instance 'Axiom' 'Text'
data instance Axiom Text
 = Axiom_Type_Text
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Text) where
	build (Axiom_Type_Text) = "Text"
instance Axiomable (Axiom Text) where
	axiom_type_of _ctx Axiom_Type_Text =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type Text where
	axiom_type = Axiom_Type_Text
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term Text)) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term Text)) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term Text)) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term Text)) where
	build (Axiom_Term t _) = build $ show t
instance Axiomable (Axiom (Axiom_Term Text)) where
	axiom_type_of _ctx (Axiom_Term _te _ty) =
		TeTy_Axiom Axiom_Type_Text

-- Instance 'Axiom' type variable

-- ** Type 'Axiom_Type_Var'

-- | Singleton type, whose constructors
-- are bijectively mapped to Haskell types
-- of kind 'Type_Var'.
data Axiom_Type_Var (v::Type_Var) where
 Axiom_Type_Var_Zero ::                     Axiom_Type_Var  'Type_Var_Zero
 Axiom_Type_Var_Succ :: Axiom_Type_Var v -> Axiom_Type_Var ('Type_Var_Succ v)
deriving instance Eq   (Axiom_Type_Var v)
deriving instance Ord  (Axiom_Type_Var v)
deriving instance Show (Axiom_Type_Var v)
deriving instance Typeable Axiom_Type_Var
instance Buildable (Axiom_Type_Var v) where
	build v = build $ type_var_string v

-- *** Type 'Type_Var'

-- | Natural numbers (aka. /Peano numbers/)
-- promoted by @DataKinds@ to Haskell type-level.
data Type_Var
 =   Type_Var_Zero
 |   Type_Var_Succ Type_Var
 deriving (Eq, Ord, Show, Typeable)

type A = Axiom_Type_Var 'Type_Var_Zero
type B = Axiom_Type_Var ('Type_Var_Succ 'Type_Var_Zero)
type C = Axiom_Type_Var ('Type_Var_Succ ('Type_Var_Succ 'Type_Var_Zero))
-- ^ …aliases only for the first few 'Axiom_Type_Var' used: extend on need.

-- | Return the Haskell term-level 'Int' encoded by the given Haskell type-level @(v :: 'Type_Var')@.
type_var_int :: Axiom_Type_Var v -> Int
type_var_int v =
	case v of
	 Axiom_Type_Var_Zero   -> 0
	 Axiom_Type_Var_Succ n -> 1 + type_var_int n

-- | Return a readable 'String' encoding the given Haskell type-level @(v :: 'Type_Var')@.
--
-- First 26 variables give: @\"A"@ to @\"Z"@,
-- and followings give: @(\"A" ++ show n)@, where @n@ is a positive 'Int' starting at @0@.
type_var_string :: Axiom_Type_Var v -> String
type_var_string v =
	case type_var_int v of
	 x | 0 <= x && x < 26 -> [Char.chr (Char.ord 'A' + x)]
	 x -> 'A' : show (x - 26)

-- *** Class 'Type_Var_Implicit'
class Type_Var_Implicit (v::Type_Var) where
	type_var :: Axiom_Type_Var v
instance Type_Var_Implicit 'Type_Var_Zero where
	type_var = Axiom_Type_Var_Zero
instance Type_Var_Implicit v => Type_Var_Implicit ('Type_Var_Succ v) where
	type_var = Axiom_Type_Var_Succ type_var

data instance Axiom (Axiom_Type_Var (v::Type_Var))
 =                   Axiom_Type_Var (Axiom_Type_Var v)
 deriving (Eq, Ord, Show)
instance Buildable (Axiom (Axiom_Type_Var (v::Type_Var))) where
	build (Axiom_Type_Var v) = build v
instance (Typeable v) => Axiomable (Axiom (Axiom_Type_Var (v::Type_Var))) where
	axiom_type_of _ctx (Axiom_Type_Var _v) =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)
instance Type_Var_Implicit v => Axiom_Type (Axiom_Type_Var (v::Type_Var)) where
	axiom_type = Axiom_Type_Var (type_var::Axiom_Type_Var v)
	axiom_Type (Axiom_Type_Var v) = TeTy_Var $ Text.pack $ type_var_string v

instance Eq (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	showsPrec n (Axiom_Term v ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		(showParen (n > 10) $
			showString "Axiom_Type_Var " .
			showsPrec n v) .
		showString " " .
		(showParen (n > 10) $
			showString " " .
			showsPrec n (ty context))
instance Buildable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	build (Axiom_Term v _ty) = build v
instance Typeable v => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	axiom_type_of ctx (Axiom_Term _ ty) = ty ctx

-- Instance 'Axiom' '->'
data instance Axiom (i -> o)
 =            Axiom_Term_Abst (Axiom i) (Axiom o)
deriving instance (Eq   (Axiom i), Eq   (Axiom o)) => Eq   (Axiom (i -> o))
deriving instance (Ord  (Axiom i), Ord  (Axiom o)) => Ord  (Axiom (i -> o))
deriving instance (Show (Axiom i), Show (Axiom o)) => Show (Axiom (i -> o))
instance (Buildable (Axiom i), Buildable (Axiom o)) => Buildable (Axiom (i -> o)) where
	build (Axiom_Term_Abst i o) =
		"(" <> build i <> " -> " <> build o <> ")"
instance
 ( Typeable i
 , Typeable o
 , Eq        (Axiom i)
 , Show      (Axiom i)
 , Buildable (Axiom i)
 , Eq        (Axiom o)
 , Show      (Axiom o)
 , Buildable (Axiom o)
 -- , Axiomable (Axiom i)
 -- , Axiomable (Axiom o)
 ) => Axiomable (Axiom (i -> o)) where
	axiom_type_of _ctx (Axiom_Term_Abst _i _o) =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance (Axiom_Type i, Axiom_Type o) => Axiom_Type (i -> o) where
	axiom_type =
		Axiom_Term_Abst
		 axiom_type
		 axiom_type
	axiom_Type (Axiom_Term_Abst i o) =
		Type_Abst ""
		(axiom_Type i) $
		(const Nothing `abstract`) $
		(axiom_Type o)
instance Eq (Axiom (Axiom_Term (i -> o))) where
	(==) = error "Eq Axiom: (==) on functions"
instance Ord (Axiom (Axiom_Term (i -> o))) where
	compare = error "Eq Axiom: compare on functions"
instance
 {-( Buildable (Axiom (i -> o))
 ) =>-} Show (Axiom (Axiom_Term (i -> o))) where
	showsPrec n (Axiom_Term _ ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showString "(_:" .
		showString (
			Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ty context)
		 ) .
		showString ")"
instance
 {-( Buildable (Axiom i)
 , Buildable (Axiom o)
 ) =>-} Buildable (Axiom (Axiom_Term (i -> o))) where
	build (Axiom_Term _o ty) =
		"(_:" <> build (ty context) <> ")"

instance
 ( Typeable (Term var)
 , Typeable o
 , Axiomable (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (Term var))
 -- , Axiomable (Axiom o)
 -- , Buildable (Axiom (Term var))
 -- , Show (Axiom (Axiom_Term (Term var)))
 -- , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Term var -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize (ctx::Context var_)
	 {-ax@-}(Axiom_Term (cast -> Just (o::Term var_ -> o)) o_ty)
	 (arg:args) =
		{-
		trace ("axiom_normalize (i -> o): Term"
		 ++ "\n ax=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ax))
		 ++ "\n ax=" ++ show ax
		 ++ "\n ty(ax)=" ++ show (typeOf ax)
		 ++ "\n arg=" ++ show (context_unlift ctx <$> arg)
		 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
		 ++ "\n o=" ++ show (Axiom_Term (o arg) o_ty)
		 ) $
		-}
		case type_of ctx arg of
		 Right i_ty ->
			case o_ty ctx of
			 Type_Abst _ _o_in o_out ->
				let oi = o arg in
				let oi_ty = const i_ty `unabstract` o_out in
				Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
			 _ -> Nothing
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Term var -> io)
 , Typeable o
 , Typeable io
 , Axiomable (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (Term var -> io))
 -- , Axiomable (Axiom o)
 -- , Show (Axiom (Axiom_Term (Term var -> io)))
 -- , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term ((Term var -> io) -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize
	 (ctx::Context var_)
	 {-ax@-}(Axiom_Term (cast -> Just (o::(Term var_ -> io) -> o)) o_ty)
	 (arg@(Term_Abst _arg_v _arg_f_in arg_f):args) =
		case type_of ctx arg of
		 Right i_ty ->
			case o_ty ctx of
			 Type_Abst _ _o_in o_out ->
				{-
				trace ("axiom_normalize (i -> o): Term ->"
				 ++ "\n ax=" ++
					(Text.unpack $
					TL.toStrict $
					Builder.toLazyText $
					build (ax))
				 ++ "\n ax=" ++ show ax
				 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
				 ++ "\n ty(args)=" ++ show (typeOf <$> args)
				 ++ "\n ty(ax)=" ++ show (typeOf ax)
				 ++ "\n i~" ++ show (typeOf (undefined::Term var -> io))
				 ++ "\n o~" ++ show (typeOf (undefined::o))
				 ++ "\n i=" ++ show (typeOf i)
				 ) $
				-}
				let i te =
					case normalize ctx (const te `unabstract` arg_f) of
					 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
					 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
				 in
				let oi = o i in
				let oi_ty = const i_ty `unabstract` o_out in
				Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
			 _ -> Nothing
		 _ -> Nothing
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): Term var -> io"
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Axiom_Type_Var v -> io)
 , Typeable o
 , Axiomable (Axiom (Axiom_Type_Var v -> io))
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (Axiom_Type_Var v -> io)))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term ((Axiom_Type_Var v -> io) -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx

instance
 ( Typeable Integer
 , Typeable o
 , Axiomable (Axiom Integer)
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term Integer))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Integer -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable Text
 , Typeable o
 , Axiomable (Axiom Text)
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term Text))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Text -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Axiom_Type_Var v)
 , Typeable o
 , Axiomable (Axiom (Axiom_Type_Var v))
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (Axiom_Type_Var v)))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var v -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (IO a)
 , Typeable o
 , Typeable a
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (IO a)))
 , Show (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (IO a))
 -- , Axiomable (Axiom o)
 ) => Axiomable (Axiom (Axiom_Term (IO a -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (Axiom_Term ((IO a) -> o)): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize (ctx::Context var)
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term (i::IO (Term var)) i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o $
				(\te ->
						case normalize ctx te of
						 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
						 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
				) <$> i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

-- ** Type 'Axiom_Type_Abst'

-- | Encode a @forall a.@ within an 'Axiom'.
data Axiom_Type_Abst
data instance Axiom (Axiom_Type_Abst)
 = Axiom_Type_Abst
   { axiom_type_abst_Var ::
    (Suggest Var_Name)
      -- ^ A name for the variable inhabiting the abstracting 'Type'.
   , axiom_type_abst_Term ::
    (Type Var_Name -> Term Var_Name)
      -- ^ The abstracted 'Term', abstracted by a 'Type'.
   , axiom_type_abst_Type ::
    (Abstraction (Suggest Var_Name) Type Var_Name)
      -- ^ The 'Type' of the abstracted 'Term'
      -- (not exactly a 'Type', but just enough to build it with 'Type_Abst').
   }
 deriving (Typeable)
instance Eq (Axiom (Axiom_Type_Abst)) where
	Axiom_Type_Abst{} == Axiom_Type_Abst{} =
		error "Eq Axiom_Type_Abst" -- maybe False (x ==) (cast y)
instance Show (Axiom (Axiom_Type_Abst)) where
	show (Axiom_Type_Abst{}) = "Axiom_Type_Abst"
instance Buildable (Axiom (Axiom_Type_Abst)) where
	build ax = "(_:" <> (build $ axiom_type_of context ax) <> ")"
instance Axiomable (Axiom (Axiom_Type_Abst)) where
	axiom_type_of ctx (Axiom_Type_Abst v _o ty) =
		Type_Abst v
		 (Type_Sort (Type_Level_0, Type_Morphism_Mono)) $
		 (context_lift ctx <$> ty)
	axiom_normalize ctx
	 {-ax@-}(Axiom_Type_Abst _ o ty)
	 (arg:args)
	 =
		let a = context_unlift ctx <$> arg in
		let ty_a = const a `unabstract` ty in
		let r = o $ ty_a in
		{-
		trace ("axiom_normalize: Axiom_Type_Abst:"
		 ++ "\n a=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (a)
			)
		 ++ "\n ty=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (axiom_type_of context ax)
			)
		 ++ "\n ty_a=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ty_a)
			)
		 ++ "\n r=" ++
			(show r
			)
		 ) $
		-}
		Just (context_lift ctx <$> r, args)
	axiom_normalize _ctx _ax _args = Nothing

-- Instance 'Axiom' 'IO'
data instance Axiom (IO a)
 = Axiom_Type_IO
 deriving (Eq, Ord, Show)
instance Buildable (Axiom (IO a)) where
	build _ = "IO"
instance (Typeable a) => Axiomable (Axiom (IO a)) where
	axiom_type_of _ctx ax =
		case ax of
		 Axiom_Type_IO ->
			 -- IO : * -> *
			Type_Abst "" (Type_Sort sort_star_mono) $
			(const Nothing `abstract`) $
			Type_Sort sort_star_mono
	axiom_eq x y =
		maybe (
			case
			 ( Typeable.splitTyConApp (typeOf x)
			 , Typeable.splitTyConApp (typeOf y)
			 ) of
			 (  (xc,[(Typeable.typeRepTyCon -> xc')])
			  , (yc,[(Typeable.typeRepTyCon -> yc')])
			  ) | xc == yc && xc' == yc' -> True
			 _ ->
				error $ "Eq: Axiomable (Axiom (IO a)): "
				 ++ "\n x : " ++ show (Typeable.splitTyConApp (typeOf x))
				 ++ "\n y : " ++ show (Typeable.splitTyConApp (typeOf y))
		 ) (x ==) (cast y)

instance
 ( Typeable a
 , Axiom_Type a
 ) => Axiom_Type (IO a) where
	axiom_type = Axiom_Type_IO
	axiom_Type (Axiom_Type_IO) =
		TeTy_App
		(TeTy_Axiom (Axiom_Type_IO::Axiom (IO a)))
		(axiom_Type (axiom_type::Axiom a))

instance Eq (Axiom (Axiom_Term (IO a))) where
	(==) = error "Eq Axiom: (==) on IO"
instance Ord (Axiom (Axiom_Term (IO a))) where
	compare = error "Eq Axiom: compare on IO"
instance
 {-( Buildable (Axiom a)
 ) =>-} Show (Axiom (Axiom_Term (IO a))) where
	showsPrec n (Axiom_Term _te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showString "(_:" .
		showString (
			Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build $ (ty context)
		 ) .
		showString ")"
instance
 {-( Buildable (Axiom a)
 ) =>-} Buildable (Axiom (Axiom_Term (IO a))) where
	build (Axiom_Term _a ty) =
		"(_:" <> build (ty context) <> ")"
instance
 ( Typeable a
 -- , Buildable (Axiom a)
 -- , Axiomable (Axiom a)
 -- , Axiomable (Axiom (Axiom_Term a))
 ) => Axiomable (Axiom (Axiom_Term (IO a))) where
	axiom_type_of ctx (Axiom_Term _a ty) = ty ctx