]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Term.hs
Add Parsing.Grammar.
[haskell/symantic.git] / 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 by 'compileO',
39 -- to enable 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 = textI1 "id"
419 const = textI2 "const"
420 flip = textI1 "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
427 ( Read_TypeNameR Text cs rs
428 , Inj_Const cs (->)
429 ) => Read_TypeNameR Text cs (Proxy (->) ': rs) where
430 read_typenameR _cs "(->)" k = k (ty @(->))
431 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
432 instance Show_Const cs => Show_Const (Proxy (->) ': cs) where
433 show_const ConstZ{} = "(->)"
434 show_const (ConstS c) = show_const c
435
436 instance -- Proj_ConC (->)
437 ( Proj_Const cs (->)
438 , Proj_Consts cs (Consts_imported_by (->))
439 , Proj_Con cs
440 ) => Proj_ConC cs (Proxy (->)) where
441 proj_conC _ (TyConst q :$ (TyConst c :$ _r))
442 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
443 , Just Refl <- proj_const c (Proxy::Proxy (->))
444 = case () of
445 _ | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
446 | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
447 | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con
448 _ -> Nothing
449 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ _a :$ b))
450 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
451 , Just Refl <- proj_const c (Proxy::Proxy (->))
452 = case () of
453 _ | Just Refl <- proj_const q (Proxy::Proxy Monoid)
454 , Just Con <- proj_con (t :$ b) -> Just Con
455 _ -> Nothing
456 proj_conC _c _q = Nothing
457 data instance TokenT meta (ts::[*]) (Proxy (->))
458 = Token_Term_Abst Name_LamVar (EToken meta '[Proxy Token_Type]) (EToken meta ts)
459 | Token_Term_App (EToken meta ts) (EToken meta ts)
460 | Token_Term_Let Name_LamVar (EToken meta ts) (EToken meta ts)
461 | Token_Term_Var Name_LamVar
462 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy (->)))
463 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy (->)))
464 instance -- CompileI (->)
465 ( Inj_Const (Consts_of_Ifaces is) (->)
466 , Read_TypeName Name_LamVar (Consts_of_Ifaces is)
467 , Compile is
468 ) => CompileI is (Proxy (->)) where
469 compileI tok ctx k =
470 case tok of
471 Token_Term_Abst name_arg tok_ty_arg tok_body ->
472 compile_type tok_ty_arg $ \(ty_arg::Type (Consts_of_Ifaces is) h) ->
473 check_kind
474 (At Nothing SKiType)
475 (At (Just $ tok_ty_arg) $ kind_of ty_arg) $ \Refl ->
476 compileO tok_body
477 (LamCtx_TypeS name_arg ty_arg ctx) $
478 \ty_res (TermO res) ->
479 k (ty_arg ~> ty_res) $ TermO $
480 \c -> lam $ \arg ->
481 res (arg `LamCtx_TermS` c)
482 Token_Term_App tok_lam tok_arg_actual ->
483 compileO tok_lam ctx $ \ty_lam (TermO lam_) ->
484 compileO tok_arg_actual ctx $ \ty_arg_actual (TermO arg_actual) ->
485 check_type2 (ty @(->)) (At (Just tok_lam) ty_lam) $ \Refl ty_arg ty_res ->
486 check_type
487 (At (Just tok_lam) ty_arg)
488 (At (Just tok_arg_actual) ty_arg_actual) $ \Refl ->
489 k ty_res $ TermO $
490 \c -> lam_ c .$ arg_actual c
491 Token_Term_Let name tok_bound tok_body ->
492 compileO tok_bound ctx $ \ty_bound (TermO bound) ->
493 compileO tok_body (LamCtx_TypeS name ty_bound ctx) $
494 \ty_res (TermO res) ->
495 k ty_res $ TermO $
496 \c -> let_ (bound c) $ \arg -> res (arg `LamCtx_TermS` c)
497 Token_Term_Var nam -> go nam ctx k
498 where
499 go :: forall meta lc ret ls rs.
500 Name_LamVar
501 -> LamCtx_Type is Name_LamVar lc
502 -> ( forall h.
503 Type (Consts_of_Ifaces is) (h::Kind.Type)
504 -> TermO lc h is ls rs
505 -> Either (Error_Term meta is) ret )
506 -> Either (Error_Term meta is) ret
507 go name lc k' =
508 case lc of
509 LamCtx_TypeZ -> Left $ Error_Term_unbound name
510 LamCtx_TypeS n typ _ | n == name ->
511 k' typ $ TermO $ \(te `LamCtx_TermS` _) -> te
512 LamCtx_TypeS _n _ty lc' ->
513 go name lc' $ \typ (TermO te::TermO lc' h is '[] is) ->
514 k' typ $ TermO $ \(_ `LamCtx_TermS` c) -> te c
515
516 -- | The function 'Type' @(->)@,
517 -- with an infix notation more readable.
518 (~>) :: forall cs a b. Inj_Const cs (->)
519 => Type cs a -> Type cs b -> Type cs (a -> b)
520 (~>) a b = ty @(->) :$ a :$ b
521 infixr 5 ~>
522
523 {-
524 -- * Class 'Sym_Type'
525 class Sym_Type term
526 instance Sym_Type term
527 type instance Sym_of_Iface (Proxy Token_Type) = Sym_Type
528 type instance Consts_of_Iface (Proxy Token_Type) = '[]
529 type instance Consts_imported_by Token_Type = '[]
530 instance -- Proj_ConC
531 Proj_ConC cs (Proxy Token_Type)
532 instance -- CompileI (->)
533 CompileI is (Proxy Token_Type) where
534 compileI _tok _ctx _k = Left $ Error_Term_unbound
535 -}