Update doc.
[haskell/symantic.git] / Language / Symantic / Compiling / Term.hs
index c0a289d7f1502d8b3f292165ff9023345ab9346e..8227e7380f2e3b386c2b354089d35b3330906707 100644 (file)
@@ -1,56 +1,42 @@
 {-# 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
+module Language.Symantic.Compiling.Term
+ ( module Language.Symantic.Compiling.Term
+ , module Language.Symantic.Compiling.Term.Grammar
+ ) 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 Data.Type.Equality ((:~:)(..))
 import GHC.Exts (Constraint)
-import Prelude hiding (not)
 
-import Language.Symantic.Lib.Data.Type.List
+import Language.Symantic.Helper.Data.Type.List
+import Language.Symantic.Parsing
 import Language.Symantic.Typing
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming.Trans
+
+import Language.Symantic.Compiling.Term.Grammar
 
 -- * Type 'Term'
--- | 'TermLC' applied on a 'LamCtx_Type'.
+-- | Closed 'TermO'.
 data Term is h
  =   Term
  (forall term. ( Sym_of_Ifaces is term
-               , Sym_Lambda term
+               , Sym_of_Iface (Proxy (->)) term
                ) => term h)
 
--- ** Type 'TermLC'
--- | A data type embedding a universal quantification
+-- ** Type 'TermO'
+-- | An open term (i.e. with a /lambda context/).
+-- The data type wraps a universal quantification
 -- over an interpreter @term@
--- and qualified by the symantics of a term.
+-- 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)
+-- built top-down by 'compileO',
+-- to enable a /Higher-Order Abstract Syntax/ (HOAS)
 -- for /lambda abstractions/ ('lam').
 --
 -- This data type is used to keep a parsed term polymorphic enough
@@ -58,21 +44,19 @@ data Term is h
 --
 -- * @(@'Sym_of_Ifaces'@ is term)@
 -- is needed when a symantic method includes a polymorphic type
--- and thus calls: 'term_from'.
+-- and thus calls: 'compileO'.
 --
 -- * @(@'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)@.
+-- make a zipper needed to be able to write the recursing 'CompileR' instance.
 --
--- * @(@'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
+-- * @(@'Sym_of_Iface'@ (@'Proxy'@ (->)) term)@
+-- is needed to handle partially applied functions.
+data TermO ctx h is ls rs
+ =   TermO
  (forall term. ( Sym_of_Ifaces is term
                , Sym_of_Ifaces ls term
                , Sym_of_Ifaces rs term
-               , Sym_Lambda term
+               , Sym_of_Iface (Proxy (->)) term
                ) => LamCtx_Term term ctx -> term h)
 
 -- * Type 'ETerm'
@@ -82,102 +66,70 @@ data ETerm is
    (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'
+-- * Type 'Compile'
+-- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
+class Compile is where
+       compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
+instance CompileR is '[] is => Compile is where
+       compileO (EToken tok) = compileR tok
+
+-- | Like 'compileO' minus for a term with an empty /lambda context/.
+compile
+ :: Compile is
+ => EToken meta is
+ -> Either (Error_Term meta is) (ETerm is)
+compile tok =
+       compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
+       Right $ ETerm typ $ Term $ te LamCtx_TermZ
+
+-- ** Type 'CompileT'
 -- | Convenient type synonym defining a term parser.
-type Term_fromT ast ctx ret is ls rs
- = ast
- -> LamCtx_Type is (Lexem ast) ctx
+type CompileT meta ctx ret is ls rs
+ = LamCtx_Type is Term_Name 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 )
+    -> TermO ctx h is ls rs
+    -> Either (Error_Term meta is) ret )
  -- ^ The accumulating continuation called bottom-up.
- -> Either (Error_Term is ast) ret
+ -> Either (Error_Term meta is) 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@.
+-- ** Class 'CompileR'
+-- | Intermediate type class to construct an instance of 'Compile'
+-- from many instances of 'CompileI', 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
+class CompileR (is::[*]) (ls::[*]) (rs::[*]) where
+       compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs
 
--- | 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'.
+-- | Recurse into into the given 'TokenR'
+-- to call the 'compileI' instance associated
+-- to the 'TokenT' it contains.
 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
+ ( CompileI is i
+ , CompileR is (i ': ls) (r ': rs)
+ ) => CompileR is ls (i ': r ': rs) where
+       compileR tok ctx k =
+               case tok of
+                TokenZ _m t -> compileI t ctx k
+                TokenS t ->
+                       compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
+                               k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
 -- | End the recursion.
-instance AST ast => Term_fromR is ls '[] ast
+instance
+ CompileI is i =>
+ CompileR is ls (i ': '[]) where
+       compileR (TokenZ _m t) ctx k = compileI t ctx k
+       compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
 
--- ** 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
+-- ** Class 'CompileI'
+-- | Handle the work of 'Compile' for a given /interface/ @i@.
+class CompileI (is::[*]) (i:: *) where
+       compileI :: TokenT meta is i -> CompileT meta ctx ret is ls (i ': rs)
 
 -- * Type family 'Sym_of_Ifaces'
 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
@@ -196,7 +148,7 @@ type family Consts_of_IfaceR (is::[*]) where
        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 family   Consts_of_Iface (i:: *) :: [*]
 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 
 -- * Type 'LamCtx_Type'
@@ -213,9 +165,6 @@ data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
                     -> 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 '[]
@@ -225,321 +174,173 @@ data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 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
+data Error_Term meta (is::[*])
+ =   Error_Term_unbound Term_Name
+ |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
+ |   Error_Term_Constraint_Type
+     (Either
+       (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
+       (Constraint_Type meta is (Consts_of_Ifaces is)))
+ |   Error_Term_Constraint_Kind (Constraint_Kind meta is)
+deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
+deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
+
+-- * Type 'Constraint_Type'
+data Constraint_Type meta ts cs
+ =   Constraint_Type_Eq  (Either (At meta '[Proxy Token_Type] (EType cs))
+                                 (At meta ts (EType cs)))
+                         (At meta ts (EType cs))
+ |   Constraint_Type_App (At meta ts (EType cs))
+ |   Constraint_Type_Con (At meta ts (KType cs Constraint))
+ |   Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
+deriving instance
+ ( Eq meta
+ , Eq_Token meta ts
+ ) => Eq (Constraint_Type meta ts cs)
+deriving instance
+ ( Show meta
+ , Show_Token meta ts
+ , Show_Const cs
+ ) => Show (Constraint_Type meta ts cs)
+
+instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
+       olift = Error_Term_Typing . olift
+instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
+       olift = Prelude.id
+instance
+ cs ~ Consts_of_Ifaces is =>
+ MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
+       olift = Error_Term_Constraint_Type . Right
+instance
+ cs ~ Consts_of_Ifaces is =>
+ MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
+       olift = Error_Term_Constraint_Type . Left
+instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
+       olift = Error_Term_Typing . Error_Type_Constraint_Kind
+instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
+       olift = Error_Term_Constraint_Kind
 
 -- ** 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
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta ts (Type cs x)
+ -> At meta ts (Type cs y)
+ -> ((x :~: y) -> Either err ret) -> Either err ret
+check_type x y k =
+       case unAt x `eq_type` unAt y of
+        Just Refl -> k Refl
+        Nothing -> Left $ olift $
+               Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
+
+check_type_is
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta '[Proxy Token_Type] (Type cs x)
+ -> At meta ts (Type cs y)
+ -> ((x :~: y) -> Either err ret) -> Either err ret
+check_type_is x y k =
+       case unAt x `eq_type` unAt y of
         Just Refl -> k Refl
-        Nothing -> Left $ Error_Term_Type_mismatch
-                (At at_x $ EType x)
-                (At at_y $ EType y)
+        Nothing -> Left $ olift $
+               Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
+
+check_type_app
+ :: MonoLift (Constraint_Type meta ts cs) err
+ => At meta ts (Type cs (fa::kfa))
+ -> (forall ka f a. (fa :~: f a)
+  -> Type cs (f::ka -> kfa)
+  -> Type cs (a::ka)
+  -> Either err ret)
+ -> Either err ret
+check_type_app typ k =
+       case unAt typ of
+        a :$ b -> k Refl a b
+        _ -> Left $ olift $
+               Constraint_Type_App (EType <$> typ)
 
--- | 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
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+    , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs (f:: * -> *)
+ -> At meta ts (Type cs fa)
+ -> (forall a. (fa :~: f a)
+  -> Type cs a
+  -> Either err ret)
+ -> Either err ret
+check_type1 typ ty_fa k =
+       check_type_app ty_fa $ \Refl ty_f ty_a ->
+       check_kind
+        (At Nothing $ SKiType `SKiArrow` SKiType)
+        (kind_of ty_f <$ ty_fa) $ \Refl ->
+       check_type
+        (At Nothing typ)
+        (ty_f <$ ty_fa) $ \Refl ->
+       k Refl ty_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
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+    , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs (f:: * -> * -> *)
+ -> At meta ts (Type cs fab)
+ -> (forall a b. (fab :~: f a b)
+  -> Type cs a
+  -> Type cs b
+  -> Either err ret)
+ -> Either err ret
+check_type2 typ ty_fab k =
+       check_type_app ty_fab            $ \Refl ty_fa ty_b ->
+       check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
+       check_kind
+        (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
+        (kind_of ty_f <$ ty_fab) $ \Refl ->
+       check_type
+        (At Nothing typ)
+        (ty_f <$ ty_fab) $ \Refl ->
+       k Refl ty_a ty_b
+
+check_con
+ :: ( Proj_Con cs
+    , MonoLift (Constraint_Type meta ts cs) err )
+ => At meta ts (Type cs (q::Constraint))
+ -> (Con q -> Either err ret)
+ -> Either err ret
+check_con typ k =
+       case proj_con $ unAt typ 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)
+        Nothing -> Left $ olift $
+               Constraint_Type_Con (KType <$> typ)
+
+check_con1
+ :: ( Proj_Con cs
+    , MonoLift (Constraint_Type meta ts cs) err
   , MonoLift (Constraint_Kind meta ts) err )
+ => Type cs con
+ -> At meta ts (Type cs (fa:: *))
+ -> (forall f a. (fa :~: f a)
   -> 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
+  -> Type cs (f:: * -> *)
+  -> Type cs (a:: *)
+  -> Either err ret)
+ -> Either err ret
+check_con1 con ty_fa k =
+       check_type_app ty_fa $ \Refl ty_f ty_a ->
+       check_kind
+        (At Nothing (SKiType `SKiArrow` SKiType))
+        (kind_of ty_f <$ ty_fa) $ \Refl ->
+       check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
+       k Refl Con ty_f ty_a
+
+check_fam
+ :: ( MonoLift (Constraint_Type meta ts cs) err
+    , Proj_Fam cs fam
+    , Show fam )
+ => At meta ts fam
+ -> Types cs hs
+ -> (Type cs (Fam fam hs) -> Either err ret)
+ -> Either err ret
+check_fam fam tys k =
+       case proj_fam (unAt fam) tys of
         Just t -> k t
-        Nothing -> Left $ error_expr is $
-               Error_Term_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
-
--}
+        Nothing -> Left $ olift $
+               Constraint_Type_Fam
+                (Text.pack . show <$> fam)
+                (etypes tys)