{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Compiling.Term where

import qualified Data.Function as Fun
import qualified Data.Kind as Kind
import Data.Kind hiding (Type)
import Data.Monoid ((<>))
import Data.Proxy (Proxy(..))
import Data.String (IsString)
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Type.Equality ((:~:)(..))
import GHC.Exts (Constraint)
import Prelude hiding (not)

import Language.Symantic.Lib.Data.Type.List
import Language.Symantic.Typing
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Type 'Term'
-- | 'TermLC' applied on a 'LamCtx_Type'.
data Term is h
 =   Term
 (forall term. ( Sym_of_Ifaces is term
               , Sym_Lambda term
               ) => term h)

-- ** Type 'TermLC'
-- | A data type embedding a universal quantification
-- over an interpreter @term@
-- and qualified by the symantics of a term.
--
-- Moreover the term is abstracted by a 'LamCtx_Term'
-- built top-down at parsing time
-- to build a /Higher-Order Abstract Syntax/ (HOAS)
-- for /lambda abstractions/ ('lam').
--
-- This data type is used to keep a parsed term polymorphic enough
-- to stay interpretable by different interpreters.
--
-- * @(@'Sym_of_Ifaces'@ is term)@
-- is needed when a symantic method includes a polymorphic type
-- and thus calls: 'term_from'.
--
-- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
-- are needed to be able to write the instance:
-- @(@'Term_fromR'@ is ls (i ': rs) ast)@.
--
-- * @(@'Sym_Lambda'@ term)@
-- is needed to be able to parse partially applied functions
-- (when their type is knowable).
data TermLC ctx h is ls rs
 =   TermLC
 (forall term. ( Sym_of_Ifaces is term
               , Sym_of_Ifaces ls term
               , Sym_of_Ifaces rs term
               , Sym_Lambda term
               ) => LamCtx_Term term ctx -> term h)

-- * Type 'ETerm'
-- | Existential 'Term', with its 'Type'.
data ETerm is
 = forall (h::Kind.Type). ETerm
   (Type (Consts_of_Ifaces is) h)
   (Term is h)

-- | Like 'term_from' but for a term with an empty /lambda context/.
root_term_from
 :: Term_from is ast
 => ast -> Either (Error_Term is ast) (ETerm is)
root_term_from ast =
	term_from ast LamCtx_TypeZ $ \ty (TermLC te) ->
	Right $ ETerm ty $ Term $ te LamCtx_TermZ

-- * Type 'Term_from'
-- | Convenient type synonym wrapping 'Term_fromR'
-- to initiate its recursion.
class Term_from is ast where
	term_from :: Term_fromT ast ctx ret is '[] is
instance
 ( AST ast
 , Eq (Lexem ast)
 , Term_fromR is '[] is ast
 ) => Term_from is ast where
	term_from ast ctx k =
		case replace_var (ast_lexem ast) ctx k of
		 Left Error_Term_unsupported -> term_fromR ast ctx k
		 x -> x
		where
		replace_var
		 :: forall lc ret.
		    Lexem ast
		 -> LamCtx_Type is (Lexem ast) lc
		 -> ( forall h.
		       Type (Consts_of_Ifaces is) (h::Kind.Type)
		    -> TermLC lc h is '[] is
		    -> Either (Error_Term is ast) ret )
		 -> Either (Error_Term is ast) ret
		replace_var name lc k' =
			case lc of
			 LamCtx_TypeZ -> Left $ Error_Term_unsupported
			 LamCtx_TypeS n ty _ | n == name ->
				k' ty $ TermLC $ \(te `LamCtx_TermS` _) -> te
			 LamCtx_TypeS _n _ty lc' ->
				replace_var name lc' $ \ty (TermLC te::TermLC lc' h is '[] is) ->
				k' ty $ TermLC $ \(_ `LamCtx_TermS` c) -> te c

-- ** Type 'Term_fromT'
-- | Convenient type synonym defining a term parser.
type Term_fromT ast ctx ret is ls rs
 = ast
 -> LamCtx_Type is (Lexem ast) ctx
 -- ^ The bound variables in scope and their types:
 -- built top-down in the heterogeneous list @ctx@,
 -- from the closest including /lambda abstraction/ to the farest.
 -> ( forall h.
       Type (Consts_of_Ifaces is) (h::Kind.Type)
    -> TermLC ctx h is ls rs
    -> Either (Error_Term is ast) ret )
 -- ^ The accumulating continuation called bottom-up.
 -> Either (Error_Term is ast) ret

-- ** Type 'Term_fromIT'
-- | Almost like 'Term_fromT', but with the remaining 'ast_nodes'
-- given to the continuation so that 'term_apply' can be used within
-- the instance 'Term_fromR'@ is ls (i ': rs) ast@.
type Term_fromIT ast ctx ret is ls rs
 = ast
 -> LamCtx_Type is (Lexem ast) ctx
 -> ( forall h.
       [ast]
    -> Type (Consts_of_Ifaces is) (h::Kind.Type)
    -> TermLC ctx h is ls rs
    -> Either (Error_Term is ast) ret )
 -> Either (Error_Term is ast) ret

-- ** Class 'Term_fromR'
-- | Intermediate type class to construct an instance of 'Term_from'
-- from many instances of 'Term_fromI', one for each item of @is@.
--
-- * @is@: starting  list of /term constants/.
-- * @ls@: done      list of /term constants/.
-- * @rs@: remaining list of /term constants/.
class Term_fromR (is::[*]) (ls::[*]) (rs::[*]) ast where
	term_fromR :: Term_fromT ast ctx ret is ls rs
	default term_fromR :: AST ast => Term_fromT ast ctx ret is ls rs
	term_fromR ast _ctx _k =
		Left $ Error_Term_unknown $
		At (Just ast) $ ast_lexem ast

-- | Test whether @i@ handles the work of 'Term_from' or not,
-- or recurse on @rs@, preserving the starting list of /term constants/,
-- and keeping a list of those done to construct 'TermLC'.
instance
 ( Term_fromI is i ast
 , Term_fromR is (i ': ls) rs ast
 , Term_from is ast
 , Inj_Const (Consts_of_Ifaces is) (->)
 ) => Term_fromR is ls (i ': rs) ast where
	term_fromR ast ctx k =
		case term_fromI ast ctx $ \as ty (TermLC te
		 ::TermLC ctx h is ls (i ': rs)) ->
			term_apply ast as ctx ty (TermLC te) k of
		 Left Error_Term_unsupported ->
			term_fromR ast ctx $ \ty (TermLC te
			 ::TermLC ctx h is (i ': ls) rs) ->
				k ty (TermLC te
				 ::TermLC ctx h is ls (i ': rs))
		 x -> x
-- | End the recursion.
instance AST ast => Term_fromR is ls '[] ast

-- | Apply the given @ast@s to the given 'TermLC',
-- or return an 'Error_Term'.
term_apply ::
 ( Term_from is ast
 , Inj_Const (Consts_of_Ifaces is) (->)
 ) => ast -> [ast]
 -> LamCtx_Type is (Lexem ast) ctx
 -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 -> TermLC ctx h is ls rs
 -> ( forall h'.
       Type (Consts_of_Ifaces is) (h' ::Kind.Type)
    -> TermLC ctx h' is ls rs
    -> Either (Error_Term is ast) ret )
 -> Either (Error_Term is ast) ret
term_apply ast_f args ctx ty_f te_f@(TermLC f) k =
	case args of
	 [] -> k ty_f te_f
	 ast_a:as ->
		term_from ast_a ctx $ \ty_a (TermLC a) ->
		check_type2 tyFun ast_f ty_f $ \Refl ty_arg ty_res ->
		check_type (At (Just ast_f) ty_arg) (At (Just ast_a) ty_a) $ \Refl ->
		term_apply ast_f as ctx ty_res (TermLC $ \c -> f c .$ a c) k

-- ** Class 'Term_fromI'
-- | Handle the work of 'Term_from' for a given /interface/ @i@,
-- that is: maybe it handles the given /interface/,
-- and if so, maybe the term can be parsed.
class Term_fromI (is::[*]) (i:: *) ast where
	term_fromI :: Term_fromIT ast ctx ret is ls (i ': rs)
	term_fromI _ast _ctx _k = Left $ Error_Term_unsupported

-- * Type family 'Sym_of_Ifaces'
type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
	Sym_of_Ifaces '[] term = ()
	Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)

-- ** Type family 'Sym_of_Iface'
type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint

-- * Type 'Consts_of_Ifaces'
type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)

-- ** Type family 'Consts_of_IfaceR'
type family Consts_of_IfaceR (is::[*]) where
	Consts_of_IfaceR '[] = '[]
	Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is

-- ** Type family 'Consts_of_Iface'
type family   Consts_of_Iface (i::k) :: [*]
type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum

-- * Type 'LamCtx_Type'
-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types (in 'Expr_From')
-- or host-terms (in 'HostI')
-- associated with the 'LamVar's in scope.
data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
	LamCtx_TypeZ :: LamCtx_Type is name '[]
	LamCtx_TypeS :: name
	             -> Type (Consts_of_Ifaces is) (h::Kind.Type)
	             -> LamCtx_Type is name hs
	             -> LamCtx_Type is name (h ': hs)
infixr 5 `LamCtx_TypeS`

-- ** Type 'LamVarName'
type LamVarName = Text

-- * Type 'LamCtx_Term'
data LamCtx_Term (term:: * -> *) (ctx::[*]) where
	LamCtx_TermZ :: LamCtx_Term term '[]
	LamCtx_TermS :: term h
	             -> LamCtx_Term term hs
	             -> LamCtx_Term term (h ': hs)
infixr 5 `LamCtx_TermS`

-- * Type 'Error_Term'
data Error_Term (is::[*]) ast
 =   Error_Term_unknown (At ast (Lexem ast))
 |   Error_Term_unsupported
 |   Error_Term_Syntax (Error_Syntax ast)
 |   Error_Term_Constraint_not_deductible (At ast (KType (Consts_of_Ifaces is) Constraint))
 |   Error_Term_Typing (At ast (Error_Type (Consts_of_Ifaces is) ast))
 |   Error_Term_Type_mismatch (At ast (EType (Consts_of_Ifaces is)))
                              (At ast (EType (Consts_of_Ifaces is)))
 |   Error_Term_Type_is_not_an_application (At ast (EType (Consts_of_Ifaces is)))
deriving instance (Eq ast, Eq (Lexem ast)) => Eq (Error_Term is ast)
deriving instance (Show ast, Show (Lexem ast), Show_Const (Consts_of_Ifaces is)) => Show (Error_Term is ast)

instance Lift_Error_Syntax (Error_Term is) where
	lift_error_syntax = Error_Term_Syntax

-- ** Checks

-- | Check that the 'kind_of' a given 'Type's equals a given kind,
-- or fail with 'Error_Type_Kind_mismatch'.
check_kind
 :: ast -> SKind k
 -> At ast (Type (Consts_of_Ifaces is) (t::kt))
 -> ((k :~: kt) -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_kind ast ki (At at_ty ty) k =
	let ki_ty = kind_of ty in
	case eq_skind ki ki_ty of
	 Just Refl -> k Refl
	 Nothing -> Left $ Error_Term_Typing $
		At (Just ast) $
		Error_Type_Kind_mismatch
		 (At Nothing $ EKind SKiType)
		 (At at_ty $ EKind ki_ty)

-- | Check that a given 'Type' is a /type application/,
-- or fail with 'Error_Term_Type_is_not_an_application'.
check_app
 :: ast -> Type (Consts_of_Ifaces is) (fx::kfx)
 -> (forall kx f x. (fx :~: f x)
  -> Type (Consts_of_Ifaces is) (f::kx -> kfx)
  -> Type (Consts_of_Ifaces is) (x::kx)
  -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_app ast ty_fx k =
	case ty_fx of
	 ty_f :$ ty_x -> k Refl ty_f ty_x
	 _ -> Left $ Error_Term_Type_is_not_an_application $
		At (Just ast) $ EType ty_fx

-- | Check that two given 'Type's are equal,
-- or fail with 'Error_Term_Type_mismatch'.
check_type
 :: At ast (Type (Consts_of_Ifaces is) x)
 -> At ast (Type (Consts_of_Ifaces is) y)
 -> ((x :~: y) -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_type (At at_x x) (At at_y y) k =
	case eq_type x y of
	 Just Refl -> k Refl
	 Nothing -> Left $ Error_Term_Type_mismatch
		 (At at_x $ EType x)
		 (At at_y $ EType y)

-- | Convenient wrapper to check for a 'Type' of kind: @* -> *@.
check_type1
 :: Type (Consts_of_Ifaces is) ty
 -> ast
 -> Type (Consts_of_Ifaces is) (fx:: *)
 -> (forall x. (fx :~: ty x)
  -> Type (Consts_of_Ifaces is) (x:: *)
  -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_type1 ty ast_ta ty_ta k =
	check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
	check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
	check_type (At Nothing ty) (At (Just ast_ta) ty_ta_t) $ \Refl ->
	k Refl ty_ta_a

-- | Convenient wrapper to check for a 'Type' of kind: @* -> * -> *@.
check_type2
 :: Type (Consts_of_Ifaces is) (ty:: * -> * -> *)
 -> ast -> Type (Consts_of_Ifaces is) a2b
 -> (forall a b. (a2b :~: (ty a b))
  -> Type (Consts_of_Ifaces is) a
  -> Type (Consts_of_Ifaces is) b
  -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_type2 ty ast ty_a2b k =
	check_app ast ty_a2b $ \Refl ty_a2b_a2 ty_a2b_b ->
	check_app ast ty_a2b_a2 $ \Refl ty_a2b_ty ty_a2b_a ->
	check_kind ast (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) (At (Just ast) ty_a2b_ty) $ \Refl ->
	check_type (At Nothing ty) (At (Just ast) ty_a2b_ty) $ \Refl ->
	k Refl ty_a2b_a ty_a2b_b

-- | Check that a given 'Constraint' holds,
-- or fail with 'Error_Term_Constraint_not_deductible'.
check_constraint
 :: Proj_Con (Consts_of_Ifaces is)
 => At ast (Type (Consts_of_Ifaces is) (q::Constraint))
 -> (Con q -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_constraint (At at_q q) k =
	case proj_con q of
	 Just Con -> k Con
	 Nothing -> Left $ Error_Term_Constraint_not_deductible $
		At at_q $ KType q

-- | Convenient wrapper to check for a 'Constraint'
-- over a 'Type' of kind: @* -> *@.
check_constraint1
 :: Proj_Con (Consts_of_Ifaces is)
 => Type (Consts_of_Ifaces is) con
 -> ast -> Type (Consts_of_Ifaces is) (fx:: *)
 -> (forall f x. (fx :~: f x)
  -> Con (con f)
  -> Type (Consts_of_Ifaces is) (f:: * -> *)
  -> Type (Consts_of_Ifaces is) (x:: *)
  -> Either (Error_Term is ast) ret)
 -> Either (Error_Term is ast) ret
check_constraint1 con ast_ta ty_ta k =
	check_app ast_ta ty_ta $ \Refl ty_ta_t ty_ta_a ->
	check_kind ast_ta (SKiType `SKiArrow` SKiType) (At (Just ast_ta) ty_ta_t) $ \Refl ->
	check_constraint (At (Just ast_ta) (con :$ ty_ta_t)) $ \Con ->
	k Refl Con ty_ta_t ty_ta_a

-- * Class 'Sym_Lambda'
class Sym_Lambda term where
	-- | /Lambda abstraction/.
	lam :: (term arg -> term res) -> term ((->) arg res)
	default lam :: Trans t term
	 => (t term arg -> t term res)
	 -> t term ((->) arg res)
	lam f = trans_lift $ lam $ trans_apply . f . trans_lift
	
	-- | /Lambda application/.
	(.$) :: term ((->) arg res) -> term arg -> term res
	default (.$) :: Trans t term
	 => t term ((->) arg res) -> t term arg -> t term res
	(.$) f x = trans_lift (trans_apply f .$ trans_apply x)
	
	-- | Convenient 'lam' and '.$' wrapper.
	let_ :: term var -> (term var -> term res) -> term res
	let_ x y = lam y .$ x
	
	id :: term a -> term a
	id a = lam Fun.id .$ a
	
	const :: term a -> term b -> term a
	const a b = lam (lam . Fun.const) .$ a .$ b
	
	-- | /Lambda composition/.
	(#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
	(#) f g = lam $ \a -> f .$ (g .$ a)
	
	flip :: term (a -> b -> c) -> term (b -> a -> c)
	flip f = lam $ \b -> lam $ \a -> f .$ a .$ b

infixl 0 .$
infixr 9 #

type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
type instance Consts_imported_by (->) =
 [ Proxy Applicative
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 ]

instance Sym_Lambda HostI where
	lam f = HostI (unHostI . f . HostI)
	(.$)  = (<*>)
instance Sym_Lambda TextI where
	lam f = TextI $ \p v ->
		let p' = Precedence 1 in
		let x = "x" <> Text.pack (show v) in
		paren p p' $ "\\" <> x <> " -> "
		 <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
	-- (.$) = textI_infix "$" (Precedence 0)
	(.$) (TextI a1) (TextI a2) =
		TextI $ \p v ->
			let p' = precedence_App in
			paren p p' $ a1 p' v <> " " <> a2 p' v
	let_ e in_ =
		TextI $ \p v ->
			let p' = Precedence 2 in
			let x = "x" <> Text.pack (show v) in
			paren p p' $ "let" <> " " <> x <> " = "
			 <> unTextI e (Precedence 0) (succ v) <> " in "
			 <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
	(#)   = textI_infix "." (Precedence 9)
	id    = textI_app1 "id"
	const = textI_app2 "const"
	flip  = textI_app1 "flip"
instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
	lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
		where lam_f = lam f
	(.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)

instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
	const_from "(->)" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
	show_const ConstZ{} = "(->)"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC (->)
 ( Proj_Const cs (->)
 , Proj_Consts cs (Consts_imported_by (->))
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy (->)) where
	proj_conC _ (TyConst q :$ (TyConst c :$ _r))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (->))
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy (->))
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ b) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI (->)
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const  (Consts_of_Ifaces is) (->)
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy (->)) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "\\" -> -- lambda abstration
			from_ast3 ast $ \ast_name ast_ty_arg ast_body as ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_arg $ \ty_arg -> Right $
			check_kind ast SKiType (At (Just ast) ty_arg) $ \Refl ->
			term_from ast_body
			 (LamCtx_TypeS (ast_lexem ast_name) ty_arg ctx) $
			 \ty_res (TermLC res) ->
			k as (ty_arg ~> ty_res) $ TermLC $
			 \c -> lam $ \arg ->
				res (arg `LamCtx_TermS` c)
		 " " -> -- lambda application
			from_ast2 ast $ \ast_lam ast_arg_actual as ->
			term_from ast_lam ctx $ \ty_lam (TermLC lam_) ->
			term_from ast_arg_actual ctx $ \ty_arg_actual (TermLC arg_actual) ->
			check_type2 tyFun ast_lam ty_lam $ \Refl ty_arg ty_res ->
			check_type
			 (At (Just ast_lam) ty_arg)
			 (At (Just ast_arg_actual) ty_arg_actual) $ \Refl ->
			k as ty_res $ TermLC $
			 \c -> lam_ c .$ arg_actual c
		 "let" ->
			from_ast3 ast $ \ast_name ast_bound ast_body as ->
			term_from ast_bound ctx $ \ty_bound (TermLC bound) ->
			term_from ast_body (LamCtx_TypeS (ast_lexem ast_name) ty_bound ctx) $
			 \ty_res (TermLC res) ->
			k as ty_res $ TermLC $
			 \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
		 _ -> Left $ Error_Term_unsupported

-- | The '(->)' 'Type'
tyFun :: Inj_Const cs (->) => Type cs (->)
tyFun = TyConst inj_const

-- | The function 'Type' @(->)@,
-- with an infix notation more readable.
(~>) :: forall cs a b. Inj_Const cs (->)
 => Type cs a -> Type cs b -> Type cs (a -> b)
(~>) a b = tyFun :$ a :$ b
infixr 5 ~>

syFun :: IsString a => [Syntax a] -> Syntax a
syFun = Syntax "(->)"

(.>) :: IsString a => Syntax a -> Syntax a -> Syntax a
a .> b = syFun [a, b]
infixr 3 .>

syLam :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
syLam arg ty body = Syntax "\\" [arg, ty, body]

syApp :: IsString a => Syntax a -> Syntax a -> Syntax a
syApp lam_ arg = Syntax " " [lam_, arg]
infixl 0 `syApp`

syLet :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
syLet name bound body = Syntax "let" [name, bound, body]

{-
-- * Checks

-- | Parsing utility to check that the type resulting
-- from the application of a given type family to a given type
-- is within the type stack,
-- or raise 'Error_Term_Type_mismatch'.
check_type0_family
 :: forall ast is tf root ty h ret.
 ( root ~ Root_of_Expr is
 , ty ~ Type_Root_of_Expr is
 , Type0_Family tf ty
 , Error_Term_Lift (Error_Term (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy tf -> Proxy is -> ast -> ty h
 -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type0_family tf is ast ty k =
	case type0_family tf ty of
	 Just t -> k t
	 Nothing -> Left $ error_expr is $
		Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast

-}