{-# 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

-- ** 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_fromR is ls (i ': rs) ast where
	term_fromR ast ctx k =
		case term_fromI ast ctx $ \ty (TermLC te
		 ::TermLC ctx h is ls (i ': rs)) ->
			k ty (TermLC te) 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

-- ** 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_fromT 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
		 "\\" ->
			from_ast3 ast $ \ast_name ast_ty_arg ast_body ->
			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 (ty_arg ~> ty_res) $ TermLC $
			 \c -> lam $ \arg ->
				res (arg `LamCtx_TermS` c)
		 " " ->
			from_ast2 ast $ \ast_lam ast_arg_actual ->
			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 ty_res $ TermLC $
			 \c -> lam_ c .$ arg_actual c
		 "let" ->
			from_ast3 ast $ \ast_name ast_bound ast_body ->
			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 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

-}