Language/Symantic/Compiling/Term.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE PolyKinds #-}
   3 {-# LANGUAGE UndecidableInstances #-}
   4 {-# OPTIONS_GHC -fno-warn-orphans #-}
   5 module Language.Symantic.Compiling.Term where
   6
   7 import qualified Data.Function as Fun
   8 import qualified Data.Kind as Kind
   9 import Data.Monoid ((<>))
  10 import Data.Proxy (Proxy(..))
  11 import Data.Text (Text)
  12 import qualified Data.Text as Text
  13 import Data.Type.Equality ((:~:)(..))
  14 import GHC.Exts (Constraint)
  15 import Prelude hiding (not)
  16
  17 import Language.Symantic.Lib.Data.Type.List
  18 import Language.Symantic.Parsing
  19 import Language.Symantic.Typing
  20 import Language.Symantic.Interpreting
  21 import Language.Symantic.Transforming.Trans
  22
  23 -- * Type 'Term'
  24 -- | Closed 'TermO'.
  25 data Term is h
  26  =   Term
  27  (forall term. ( Sym_of_Ifaces is term
  28                , Sym_Lambda term
  29                ) => term h)
  30
  31 -- ** Type 'TermO'
  32 -- | An open term (i.e. with a /lambda context/).
  33 -- The data type wraps a universal quantification
  34 -- over an interpreter @term@
  35 -- qualified by the symantics of a term.
  36 --
  37 -- Moreover the term is abstracted by a 'LamCtx_Term'
  38 -- built top-down at by 'compileO'
  39 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
  40 -- for /lambda abstractions/ ('lam').
  41 --
  42 -- This data type is used to keep a parsed term polymorphic enough
  43 -- to stay interpretable by different interpreters.
  44 --
  45 -- * @(@'Sym_of_Ifaces'@ is term)@
  46 -- is needed when a symantic method includes a polymorphic type
  47 -- and thus calls: 'compileO'.
  48 --
  49 -- * @(@'Sym_of_Ifaces'@ ls term)@ and @(@'Sym_of_Ifaces'@ rs term)@
  50 -- make a zipper needed to be able to write the recursing 'CompileR' instance.
  51 --
  52 -- * @(@'Sym_Lambda'@ term)@
  53 -- is needed to handle partially applied functions.
  54 data TermO ctx h is ls rs
  55  =   TermO
  56  (forall term. ( Sym_of_Ifaces is term
  57                , Sym_of_Ifaces ls term
  58                , Sym_of_Ifaces rs term
  59                , Sym_Lambda term
  60                ) => LamCtx_Term term ctx -> term h)
  61
  62 -- * Type 'ETerm'
  63 -- | Existential 'Term', with its 'Type'.
  64 data ETerm is
  65  = forall (h::Kind.Type). ETerm
  66    (Type (Consts_of_Ifaces is) h)
  67    (Term is h)
  68
  69 -- * Type 'Compile'
  70 -- | Convenient type synonym wrapping 'CompileR' to initiate its recursion.
  71 class Compile is where
  72         compileO :: EToken meta is -> CompileT meta ctx ret is '[] is
  73 instance CompileR is '[] is => Compile is where
  74         compileO (EToken tok) = compileR tok
  75
  76 -- | Like 'compileO' but for a term with an empty /lambda context/.
  77 compile
  78  :: Compile is
  79  => EToken meta is
  80  -> Either (Error_Term meta is) (ETerm is)
  81 compile tok =
  82         compileO tok LamCtx_TypeZ $ \typ (TermO te) ->
  83         Right $ ETerm typ $ Term $ te LamCtx_TermZ
  84
  85 -- ** Type 'CompileT'
  86 -- | Convenient type synonym defining a term parser.
  87 type CompileT meta ctx ret is ls rs
  88  = LamCtx_Type is Name_LamVar ctx
  89  -- ^ The bound variables in scope and their types:
  90  -- built top-down in the heterogeneous list @ctx@,
  91  -- from the closest including /lambda abstraction/ to the farest.
  92  -> ( forall h.
  93        Type (Consts_of_Ifaces is) (h::Kind.Type)
  94     -> TermO ctx h is ls rs
  95     -> Either (Error_Term meta is) ret )
  96  -- ^ The accumulating continuation called bottom-up.
  97  -> Either (Error_Term meta is) ret
  98
  99 -- ** Class 'CompileR'
 100 -- | Intermediate type class to construct an instance of 'Compile'
 101 -- from many instances of 'CompileI', one for each item of @is@.
 102 --
 103 -- * @is@: starting  list of /term constants/.
 104 -- * @ls@: done      list of /term constants/.
 105 -- * @rs@: remaining list of /term constants/.
 106 class CompileR (is::[*]) (ls::[*]) (rs::[*]) where
 107         compileR :: TokenR meta is rs i -> CompileT meta ctx ret is ls rs
 108
 109 -- | Recurse into into the given 'TokenR'
 110 -- to call the 'compileI' instance associated
 111 -- to the 'TokenT' it contains.
 112 instance
 113  ( CompileI is i
 114  , CompileR is (i ': ls) (r ': rs)
 115  ) => CompileR is ls (i ': r ': rs) where
 116         compileR tok ctx k =
 117                 case tok of
 118                  TokenZ _m t -> compileI t ctx k
 119                  TokenS t ->
 120                         compileR t ctx $ \typ (TermO te :: TermO ctx h is (i ': ls) (r ': rs)) ->
 121                                 k typ (TermO te :: TermO ctx h is ls (i ': r ': rs))
 122 -- | End the recursion.
 123 instance
 124  CompileI is i =>
 125  CompileR is ls (i ': '[]) where
 126         compileR (TokenZ _m t) ctx k = compileI t ctx k
 127         compileR TokenS{} _ctx _k = error "Oops, the impossible happened..."
 128
 129 -- ** Class 'CompileI'
 130 -- | Handle the work of 'Compile' for a given /interface/ @i@.
 131 class CompileI (is::[*]) (i:: *) where
 132         compileI :: TokenT meta is i -> CompileT meta ctx ret is ls (i ': rs)
 133
 134 -- * Type family 'Sym_of_Ifaces'
 135 type family Sym_of_Ifaces (is::[*]) (term:: * -> *) :: Constraint where
 136         Sym_of_Ifaces '[] term = ()
 137         Sym_of_Ifaces (i ': is) term = (Sym_of_Iface i term, Sym_of_Ifaces is term)
 138
 139 -- ** Type family 'Sym_of_Iface'
 140 type family Sym_of_Iface (i:: *) :: {-term-}(* -> *) -> Constraint
 141
 142 -- * Type 'Consts_of_Ifaces'
 143 type Consts_of_Ifaces is = Nub (Consts_of_IfaceR is)
 144
 145 -- ** Type family 'Consts_of_IfaceR'
 146 type family Consts_of_IfaceR (is::[*]) where
 147         Consts_of_IfaceR '[] = '[]
 148         Consts_of_IfaceR (i ': is) = Consts_of_Iface i ++ Consts_of_IfaceR is
 149
 150 -- ** Type family 'Consts_of_Iface'
 151 type family   Consts_of_Iface (i:: *) :: [*]
 152 type instance Consts_of_Iface (Proxy Enum) = Proxy Enum ': Consts_imported_by Enum
 153
 154 -- * Type 'LamCtx_Type'
 155 -- | GADT for a typing context,
 156 -- accumulating an @item@ at each lambda;
 157 -- used to accumulate object-types (in 'Expr_From')
 158 -- or host-terms (in 'HostI')
 159 -- associated with the 'LamVar's in scope.
 160 data LamCtx_Type (is::[*]) (name:: *) (ctx::[*]) where
 161         LamCtx_TypeZ :: LamCtx_Type is name '[]
 162         LamCtx_TypeS :: name
 163                      -> Type (Consts_of_Ifaces is) (h::Kind.Type)
 164                      -> LamCtx_Type is name hs
 165                      -> LamCtx_Type is name (h ': hs)
 166 infixr 5 `LamCtx_TypeS`
 167
 168 -- ** Type 'Name_LamVar'
 169 type Name_LamVar = Text
 170
 171 -- * Type 'LamCtx_Term'
 172 data LamCtx_Term (term:: * -> *) (ctx::[*]) where
 173         LamCtx_TermZ :: LamCtx_Term term '[]
 174         LamCtx_TermS :: term h
 175                      -> LamCtx_Term term hs
 176                      -> LamCtx_Term term (h ': hs)
 177 infixr 5 `LamCtx_TermS`
 178
 179 -- * Type 'Error_Term'
 180 data Error_Term meta (is::[*])
 181  =   Error_Term_unbound Name_LamVar
 182  |   Error_Term_Typing (Error_Type meta '[Proxy Token_Type])
 183  |   Error_Term_Constraint_Type
 184      (Either
 185        (Constraint_Type meta '[Proxy Token_Type] (Consts_of_Ifaces is))
 186        (Constraint_Type meta is (Consts_of_Ifaces is)))
 187  |   Error_Term_Constraint_Kind (Constraint_Kind meta is)
 188 deriving instance (Eq meta, Eq_Token meta is) => Eq (Error_Term meta is)
 189 deriving instance (Show meta, Show_Token meta is, Show_Const (Consts_of_Ifaces is)) => Show (Error_Term meta is)
 190
 191 -- * Type 'Constraint_Type'
 192 data Constraint_Type meta ts cs
 193  =   Constraint_Type_Eq  (Either (At meta '[Proxy Token_Type] (EType cs))
 194                                  (At meta ts (EType cs)))
 195                          (At meta ts (EType cs))
 196  |   Constraint_Type_App (At meta ts (EType cs))
 197  |   Constraint_Type_Con (At meta ts (KType cs Constraint))
 198  |   Constraint_Type_Fam (At meta ts Name_Fam) [EType cs]
 199 deriving instance
 200  ( Eq meta
 201  , Eq_Token meta ts
 202  ) => Eq (Constraint_Type meta ts cs)
 203 deriving instance
 204  ( Show meta
 205  , Show_Token meta ts
 206  , Show_Const cs
 207  ) => Show (Constraint_Type meta ts cs)
 208
 209
 210 instance MonoLift (Error_Type meta '[Proxy Token_Type]) (Error_Term meta ts) where
 211         olift = Error_Term_Typing . olift
 212 instance MonoLift (Error_Term meta ts) (Error_Term meta ts) where
 213         olift = Prelude.id
 214 instance
 215  cs ~ Consts_of_Ifaces is =>
 216  MonoLift (Constraint_Type meta is cs) (Error_Term meta is) where
 217         olift = Error_Term_Constraint_Type . Right
 218 instance
 219  cs ~ Consts_of_Ifaces is =>
 220  MonoLift (Constraint_Type meta '[Proxy Token_Type] cs) (Error_Term meta is) where
 221         olift = Error_Term_Constraint_Type . Left
 222 instance MonoLift (Constraint_Kind meta '[Proxy Token_Type]) (Error_Term meta is) where
 223         olift = Error_Term_Typing . Error_Type_Constraint_Kind
 224 instance MonoLift (Constraint_Kind meta is) (Error_Term meta is) where
 225         olift = Error_Term_Constraint_Kind
 226
 227 -- ** Checks
 228 check_type
 229  :: MonoLift (Constraint_Type meta ts cs) err
 230  => At meta ts (Type cs x)
 231  -> At meta ts (Type cs y)
 232  -> ((x :~: y) -> Either err ret) -> Either err ret
 233 check_type x y k =
 234         case unAt x `eq_type` unAt y of
 235          Just Refl -> k Refl
 236          Nothing -> Left $ olift $
 237                 Constraint_Type_Eq (Right $ EType <$> x) (EType <$> y)
 238
 239 check_type_is
 240  :: MonoLift (Constraint_Type meta ts cs) err
 241  => At meta '[Proxy Token_Type] (Type cs x)
 242  -> At meta ts (Type cs y)
 243  -> ((x :~: y) -> Either err ret) -> Either err ret
 244 check_type_is x y k =
 245         case unAt x `eq_type` unAt y of
 246          Just Refl -> k Refl
 247          Nothing -> Left $ olift $
 248                 Constraint_Type_Eq (Left $ EType <$> x) (EType <$> y)
 249
 250 check_type_app
 251  :: MonoLift (Constraint_Type meta ts cs) err
 252  => At meta ts (Type cs (fa::kfa))
 253  -> (forall ka f a. (fa :~: f a)
 254   -> Type cs (f::ka -> kfa)
 255   -> Type cs (a::ka)
 256   -> Either err ret)
 257  -> Either err ret
 258 check_type_app typ k =
 259         case unAt typ of
 260          a :$ b -> k Refl a b
 261          _ -> Left $ olift $
 262                 Constraint_Type_App (EType <$> typ)
 263
 264 check_type1
 265  :: ( MonoLift (Constraint_Type meta ts cs) err
 266     , MonoLift (Constraint_Kind meta ts) err )
 267  => Type cs (f:: * -> *)
 268  -> At meta ts (Type cs fa)
 269  -> (forall a. (fa :~: f a)
 270   -> Type cs a
 271   -> Either err ret)
 272  -> Either err ret
 273 check_type1 typ ty_fa k =
 274         check_type_app ty_fa $ \Refl ty_f ty_a ->
 275         check_kind
 276          (At Nothing $ SKiType `SKiArrow` SKiType)
 277          (kind_of ty_f <$ ty_fa) $ \Refl ->
 278         check_type
 279          (At Nothing typ)
 280          (ty_f <$ ty_fa) $ \Refl ->
 281         k Refl ty_a
 282
 283 check_type2
 284  :: ( MonoLift (Constraint_Type meta ts cs) err
 285     , MonoLift (Constraint_Kind meta ts) err )
 286  => Type cs (f:: * -> * -> *)
 287  -> At meta ts (Type cs fab)
 288  -> (forall a b. (fab :~: f a b)
 289   -> Type cs a
 290   -> Type cs b
 291   -> Either err ret)
 292  -> Either err ret
 293 check_type2 typ ty_fab k =
 294         check_type_app ty_fab            $ \Refl ty_fa ty_b ->
 295         check_type_app (ty_fa <$ ty_fab) $ \Refl ty_f  ty_a ->
 296         check_kind
 297          (At Nothing $ SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 298          (kind_of ty_f <$ ty_fab) $ \Refl ->
 299         check_type
 300          (At Nothing typ)
 301          (ty_f <$ ty_fab) $ \Refl ->
 302         k Refl ty_a ty_b
 303
 304 check_con
 305  :: ( Proj_Con cs
 306     , MonoLift (Constraint_Type meta ts cs) err )
 307  => At meta ts (Type cs (q::Constraint))
 308  -> (Con q -> Either err ret)
 309  -> Either err ret
 310 check_con typ k =
 311         case proj_con $ unAt typ of
 312          Just Con -> k Con
 313          Nothing -> Left $ olift $
 314                 Constraint_Type_Con (KType <$> typ)
 315
 316 check_con1
 317  :: ( Proj_Con cs
 318     , MonoLift (Constraint_Type meta ts cs) err
 319     , MonoLift (Constraint_Kind meta ts) err )
 320  => Type cs con
 321  -> At meta ts (Type cs (fa:: *))
 322  -> (forall f a. (fa :~: f a)
 323   -> Con (con f)
 324   -> Type cs (f:: * -> *)
 325   -> Type cs (a:: *)
 326   -> Either err ret)
 327  -> Either err ret
 328 check_con1 con ty_fa k =
 329         check_type_app ty_fa $ \Refl ty_f ty_a ->
 330         check_kind
 331          (At Nothing (SKiType `SKiArrow` SKiType))
 332          (kind_of ty_f <$ ty_fa) $ \Refl ->
 333         check_con ((con :$ ty_f) <$ ty_fa) $ \Con ->
 334         k Refl Con ty_f ty_a
 335
 336 check_fam
 337  :: ( MonoLift (Constraint_Type meta ts cs) err
 338     , Proj_Fam cs fam
 339     , Show fam )
 340  => At meta ts fam
 341  -> Types cs hs
 342  -> (Type cs (Fam fam hs) -> Either err ret)
 343  -> Either err ret
 344 check_fam fam tys k =
 345         case proj_fam (unAt fam) tys of
 346          Just t -> k t
 347          Nothing -> Left $ olift $
 348                 Constraint_Type_Fam
 349                  (Text.pack . show <$> fam)
 350                  (etypes tys)
 351
 352 -- * Class 'Sym_Lambda'
 353 class Sym_Lambda term where
 354         -- | /Lambda abstraction/.
 355         lam :: (term arg -> term res) -> term ((->) arg res)
 356         default lam :: Trans t term
 357          => (t term arg -> t term res)
 358          -> t term ((->) arg res)
 359         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 360
 361         -- | /Lambda application/.
 362         (.$) :: term ((->) arg res) -> term arg -> term res
 363         default (.$) :: Trans t term
 364          => t term ((->) arg res) -> t term arg -> t term res
 365         (.$) f x = trans_lift (trans_apply f .$ trans_apply x)
 366
 367         -- | Convenient 'lam' and '.$' wrapper.
 368         let_ :: term var -> (term var -> term res) -> term res
 369         let_ x y = lam y .$ x
 370
 371         id :: term a -> term a
 372         id a = lam Fun.id .$ a
 373
 374         const :: term a -> term b -> term a
 375         const a b = lam (lam . Fun.const) .$ a .$ b
 376
 377         -- | /Lambda composition/.
 378         (#) :: term (b -> c) -> term (a -> b) -> term (a -> c)
 379         (#) f g = lam $ \a -> f .$ (g .$ a)
 380
 381         flip :: term (a -> b -> c) -> term (b -> a -> c)
 382         flip f = lam $ \b -> lam $ \a -> f .$ a .$ b
 383
 384 infixl 0 .$
 385 infixr 9 #
 386
 387 type instance Sym_of_Iface (Proxy (->)) = Sym_Lambda
 388 type instance Consts_of_Iface (Proxy (->)) = Proxy (->) ': Consts_imported_by (->)
 389 type instance Consts_imported_by (->) =
 390  [ Proxy Applicative
 391  , Proxy Functor
 392  , Proxy Monad
 393  , Proxy Monoid
 394  ]
 395
 396 instance Sym_Lambda HostI where
 397         lam f = HostI (unHostI . f . HostI)
 398         (.$)  = (<*>)
 399 instance Sym_Lambda TextI where
 400         lam f = TextI $ \p v ->
 401                 let p' = Precedence 1 in
 402                 let x = "x" <> Text.pack (show v) in
 403                 paren p p' $ "\\" <> x <> " -> "
 404                  <> unTextI (f (TextI $ \_p _v -> x)) p' (succ v)
 405         -- (.$) = textI_infix "$" (Precedence 0)
 406         (.$) (TextI a1) (TextI a2) =
 407                 TextI $ \p v ->
 408                         let p' = precedence_App in
 409                         paren p p' $ a1 p' v <> " " <> a2 p' v
 410         let_ e in_ =
 411                 TextI $ \p v ->
 412                         let p' = Precedence 2 in
 413                         let x = "x" <> Text.pack (show v) in
 414                         paren p p' $ "let" <> " " <> x <> " = "
 415                          <> unTextI e (Precedence 0) (succ v) <> " in "
 416                          <> unTextI (in_ (TextI $ \_p _v -> x)) p' (succ v)
 417         (#)   = textI_infix "." (Precedence 9)
 418         id    = textI_app1 "id"
 419         const = textI_app2 "const"
 420         flip  = textI_app1 "flip"
 421 instance (Sym_Lambda r1, Sym_Lambda r2) => Sym_Lambda (DupI r1 r2) where
 422         lam f = dupI_1 lam_f `DupI` dupI_2 lam_f
 423                 where lam_f = lam f
 424         (.$) = dupI2 (Proxy::Proxy Sym_Lambda) (.$)
 425
 426 instance Const_from Text cs => Const_from Text (Proxy (->) ': cs) where
 427         const_from "(->)" k = k (ConstZ kind)
 428         const_from s k = const_from s $ k . ConstS
 429 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
 430         show_const ConstZ{} = "(->)"
 431         show_const (ConstS c) = show_const c
 432
 433 instance -- Proj_ConC (->)
 434  ( Proj_Const cs (->)
 435  , Proj_Consts cs (Consts_imported_by (->))
 436  , Proj_Con cs
 437  ) => Proj_ConC cs (Proxy (->)) where
 438         proj_conC _ (TyConst q :$ (TyConst c :$ _r))
 439          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 440          , Just Refl <- proj_const c (Proxy::Proxy (->))
 441          = case () of
 442                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 443                    | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
 444                    | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
 445                  _ -> Nothing
 446         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
 447          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 448          , Just Refl <- proj_const c (Proxy::Proxy (->))
 449          = case () of
 450                  _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 451                    , Just Con  <- proj_con (t :$ b) -> Just Con
 452                  _ -> Nothing
 453         proj_conC _c _q = Nothing
 454 data instance TokenT meta (ts::[*]) (Proxy (->))
 455  = Token_Term_Abst Name_LamVar (EToken meta '[Proxy Token_Type]) (EToken meta ts)
 456  | Token_Term_App              (EToken meta ts) (EToken meta ts)
 457  | Token_Term_Let  Name_LamVar (EToken meta ts) (EToken meta ts)
 458  | Token_Term_Var  Name_LamVar
 459 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
 460 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
 461 instance -- CompileI (->)
 462  ( Inj_Const  (Consts_of_Ifaces is) (->)
 463  , Const_from Name_LamVar (Consts_of_Ifaces is)
 464  , Compile is
 465  ) => CompileI is (Proxy (->)) where
 466         compileI tok ctx k =
 467                 case tok of
 468                  Token_Term_Abst name_arg tok_ty_arg tok_body ->
 469                         type_from tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
 470                         check_kind
 471                          (At Nothing SKiType)
 472                          (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
 473                         compileO tok_body
 474                          (LamCtx_TypeS name_arg ty_arg ctx) $
 475                          \ty_res (TermO res) ->
 476                         k (ty_arg ~> ty_res) $ TermO $
 477                          \c -> lam $ \arg ->
 478                                 res (arg `LamCtx_TermS` c)
 479                  Token_Term_App tok_lam tok_arg_actual ->
 480                         compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
 481                         compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
 482                         check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
 483                         check_type
 484                          (At (Just tok_lam) ty_arg)
 485                          (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
 486                         k ty_res $ TermO $
 487                          \c -> lam_ c .$ arg_actual c
 488                  Token_Term_Let name tok_bound tok_body ->
 489                         compileO tok_bound ctx $ \ty_bound (TermO bound) ->
 490                         compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
 491                          \ty_res (TermO res) ->
 492                         k ty_res $ TermO $
 493                          \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
 494                  Token_Term_Var nam -> go nam ctx k
 495                         where
 496                         go :: forall meta lc ret ls rs.
 497                             Name_LamVar
 498                          -> LamCtx_Type is Name_LamVar lc
 499                          -> ( forall h.
 500                                Type (Consts_of_Ifaces is) (h::Kind.Type)
 501                             -> TermO lc h is ls rs
 502                             -> Either (Error_Term meta is) ret )
 503                          -> Either (Error_Term meta is) ret
 504                         go name lc k' =
 505                                 case lc of
 506                                  LamCtx_TypeZ -> Left $ Error_Term_unbound name
 507                                  LamCtx_TypeS n typ _ | n == name ->
 508                                         k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
 509                                  LamCtx_TypeS _n _ty lc' ->
 510                                         go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
 511                                         k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
 512
 513 -- | The function 'Type' @(->)@,
 514 -- with an infix notation more readable.
 515 (~>) :: forall cs a b. Inj_Const cs (->)
 516  => Type cs a -> Type cs b -> Type cs (a -> b)
 517 (~>) a b = ty @(->) :$ a :$ b
 518 infixr 5 ~>
 519
 520 {-
 521 -- * Class 'Sym_Type'
 522 class Sym_Type term
 523 instance Sym_Type term
 524 type instance Sym_of_Iface (Proxy Token_Type) = Sym_Type
 525 type instance Consts_of_Iface (Proxy Token_Type) = '[]
 526 type instance Consts_imported_by Token_Type = '[]
 527 instance -- Proj_ConC
 528  Proj_ConC cs (Proxy Token_Type)
 529 instance -- CompileI (->)
 530  CompileI is (Proxy Token_Type) where
 531         compileI _tok _ctx _k = Left $ Error_Term_unbound
 532 -}