Skip to main content

hyperlight_component_util/
substitute.rs

1// SPDX-License-Identifier: Apache-2.0
2// Copyright 2025 The Hyperlight Authors.
3
4//! Capture-avoiding substitution
5
6use std::primitive::u32;
7
8use crate::etypes::{
9    BoundedTyvar, Component, Ctx, Defined, ExternDecl, ExternDesc, FreeTyvar, Func, Handleable,
10    Instance, Param, QualifiedInstance, RecordField, TypeBound, Tyvar, Value, VariantCase,
11};
12use crate::tv::ResolvedTyvar;
13
14/// A substitution
15///
16/// This trait can be implemented by specific structures that have
17/// specific substitution behavior, which only need to define how the
18/// act on bound/existential/universal variables. The implemented
19/// methods on the trait will then allow applying that substitution in
20/// a capture-avoiding manner to any relevant term.
21///
22/// The [`Shiftable`] bound is required because the implementation of
23/// substitution for components and instances needs to be able to
24/// shift the substitution in order to make substitution
25/// capture-avoiding.
26pub trait Substitution<'a>
27where
28    Self: Shiftable<'a>,
29{
30    /// Some, but not all, substitutions are fallible (i.e. may reveal
31    /// latent misbehaviour in the type they are being applied to), so
32    /// any given [`Substitution`] can provide its own
33    /// [`Substitution::Error`] type.
34    ///
35    /// An infallible substitution can use [`Void`] to reflect
36    /// the fact that error is impossible, and callers can use
37    /// [`Unvoidable::not_void`] to eliminate the impossible case of
38    /// the result neatly.
39    type Error: From<<<Self as Shiftable<'a>>::Inner as Substitution<'a>>::Error>;
40    /// Any substitution should define whether a given bound variable
41    /// should be substituted, and if so with what.
42    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
43    /// Any substitution should define whether a given existential variable
44    /// should be substituted, and if so with what.
45    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
46    /// Any substitution should define whether a given universal variable
47    /// should be substituted, and if so with what.
48    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
49
50    fn record_fields(&self, rfs: &[RecordField<'a>]) -> Result<Vec<RecordField<'a>>, Self::Error> {
51        rfs.iter()
52            .map(|rf| {
53                Ok(RecordField {
54                    name: rf.name,
55                    ty: self.value(&rf.ty)?,
56                })
57            })
58            .collect()
59    }
60
61    fn variant_cases(&self, vcs: &[VariantCase<'a>]) -> Result<Vec<VariantCase<'a>>, Self::Error> {
62        vcs.iter()
63            .map(|vc| {
64                Ok(VariantCase {
65                    name: vc.name,
66                    ty: self.value_option(&vc.ty)?,
67                })
68            })
69            .collect()
70    }
71
72    fn value_option(&self, vt: &Option<Value<'a>>) -> Result<Option<Value<'a>>, Self::Error> {
73        vt.as_ref().map(|ty| self.value(ty)).transpose()
74    }
75
76    fn value(&self, vt: &Value<'a>) -> Result<Value<'a>, Self::Error> {
77        Ok(match vt {
78            Value::Bool => Value::Bool,
79            Value::S(w) => Value::S(*w),
80            Value::U(w) => Value::U(*w),
81            Value::F(w) => Value::F(*w),
82            Value::Char => Value::Char,
83            Value::String => Value::String,
84            Value::List(vt) => Value::List(Box::new(self.value(vt)?)),
85            Value::FixList(vt, size) => Value::FixList(Box::new(self.value(vt)?), *size),
86            Value::Record(rfs) => Value::Record(self.record_fields(rfs)?),
87            Value::Variant(vcs) => Value::Variant(self.variant_cases(vcs)?),
88            Value::Flags(ns) => Value::Flags(ns.clone()),
89            Value::Enum(ns) => Value::Enum(ns.clone()),
90            Value::Option(vt) => Value::Option(Box::new(self.value(vt)?)),
91            Value::Tuple(vts) => Value::Tuple(
92                vts.iter()
93                    .map(|vt| self.value(vt))
94                    .collect::<Result<Vec<Value<'a>>, Self::Error>>()?,
95            ),
96            Value::Result(vt1, vt2) => Value::Result(
97                Box::new(self.value_option(vt1)?),
98                Box::new(self.value_option(vt2)?),
99            ),
100            Value::Own(h) => Value::Own(self.handleable_(h)?),
101            Value::Borrow(h) => Value::Borrow(self.handleable_(h)?),
102            Value::Var(tv, vt) => Value::Var(
103                tv.as_ref().and_then(|tv| match self.var(tv) {
104                    Ok(Some(Defined::Handleable(Handleable::Var(tv)))) => Some(tv),
105                    Ok(None) => Some(tv.clone()),
106                    _ => None,
107                }),
108                Box::new(self.value(vt)?),
109            ),
110        })
111    }
112
113    fn param(&self, pt: &Param<'a>) -> Result<Param<'a>, Self::Error> {
114        Ok(Param {
115            name: pt.name,
116            ty: self.value(&pt.ty)?,
117        })
118    }
119
120    fn params(&self, pts: &Vec<Param<'a>>) -> Result<Vec<Param<'a>>, Self::Error> {
121        pts.iter().map(|pt| self.param(pt)).collect()
122    }
123
124    fn result(
125        &self,
126        rt: &crate::etypes::Result<'a>,
127    ) -> Result<crate::etypes::Result<'a>, Self::Error> {
128        Ok(match rt {
129            Some(vt) => Some(self.value(vt)?),
130            None => None,
131        })
132    }
133
134    fn func(&self, ft: &Func<'a>) -> Result<Func<'a>, Self::Error> {
135        Ok(Func {
136            params: self.params(&ft.params)?,
137            result: self.result(&ft.result)?,
138        })
139    }
140
141    fn var(&self, tv: &Tyvar) -> Result<Option<Defined<'a>>, Self::Error> {
142        match tv {
143            Tyvar::Bound(i) => self.subst_bvar(*i),
144            Tyvar::Free(FreeTyvar::U(o, i)) => self.subst_uvar(*o, *i),
145            Tyvar::Free(FreeTyvar::E(o, i)) => self.subst_evar(*o, *i),
146        }
147    }
148
149    fn handleable(&self, h: &Handleable) -> Result<Defined<'a>, Self::Error> {
150        let hh = Defined::Handleable(h.clone());
151        match h {
152            Handleable::Resource(_) => Ok(hh),
153            Handleable::Var(tv) => Ok(self.var(tv)?.unwrap_or(hh)),
154        }
155    }
156
157    fn handleable_(&self, h: &Handleable) -> Result<Handleable, Self::Error> {
158        match self.handleable(h)? {
159            Defined::Handleable(h_) => Ok(h_),
160            _ => panic!("internal invariant a violation: owned/borrowed var is not resource"),
161        }
162    }
163
164    fn defined(&self, dt: &Defined<'a>) -> Result<Defined<'a>, Self::Error> {
165        Ok(match dt {
166            Defined::Handleable(h) => self.handleable(h)?,
167            Defined::Value(vt) => Defined::Value(self.value(vt)?),
168            Defined::Func(ft) => Defined::Func(self.func(ft)?),
169            Defined::Instance(it) => Defined::Instance(self.qualified_instance(it)?),
170            Defined::Component(ct) => Defined::Component(self.component(ct)?),
171        })
172    }
173
174    fn type_bound(&self, tb: &TypeBound<'a>) -> Result<TypeBound<'a>, Self::Error> {
175        Ok(match tb {
176            TypeBound::Eq(dt) => TypeBound::Eq(self.defined(dt)?),
177            TypeBound::SubResource => TypeBound::SubResource,
178        })
179    }
180
181    fn bounded_tyvar(&self, btv: &BoundedTyvar<'a>) -> Result<BoundedTyvar<'a>, Self::Error> {
182        Ok(BoundedTyvar {
183            origin: btv.origin.clone(),
184            bound: self.type_bound(&btv.bound)?,
185        })
186    }
187
188    fn extern_desc(&self, ed: &ExternDesc<'a>) -> Result<ExternDesc<'a>, Self::Error> {
189        Ok(match ed {
190            ExternDesc::CoreModule(cmt) => ExternDesc::CoreModule(cmt.clone()),
191            ExternDesc::Func(ft) => ExternDesc::Func(self.func(ft)?),
192            ExternDesc::Type(dt) => ExternDesc::Type(self.defined(dt)?),
193            ExternDesc::Instance(it) => ExternDesc::Instance(self.instance(it)?),
194            ExternDesc::Component(ct) => ExternDesc::Component(self.component(ct)?),
195        })
196    }
197
198    fn extern_decl(&self, ed: &ExternDecl<'a>) -> Result<ExternDecl<'a>, Self::Error> {
199        Ok(ExternDecl {
200            kebab_name: ed.kebab_name,
201            desc: self.extern_desc(&ed.desc)?,
202        })
203    }
204
205    fn instance(&self, it: &Instance<'a>) -> Result<Instance<'a>, Self::Error> {
206        let exports = it
207            .exports
208            .iter()
209            .map(|ed| self.extern_decl(ed))
210            .collect::<Result<Vec<_>, Self::Error>>()?;
211        Ok(Instance { exports })
212    }
213
214    fn qualified_instance(
215        &self,
216        qit: &QualifiedInstance<'a>,
217    ) -> Result<QualifiedInstance<'a>, Self::Error> {
218        let mut evars = Vec::new();
219        let mut sub = self.shifted();
220        for evar in &qit.evars {
221            evars.push(sub.bounded_tyvar(evar)?);
222            sub.bshift(1);
223            sub.rbshift(1);
224        }
225        let it = sub.instance(&qit.unqualified)?;
226        Ok(QualifiedInstance {
227            evars,
228            unqualified: it,
229        })
230    }
231
232    fn component(&self, ct: &Component<'a>) -> Result<Component<'a>, Self::Error> {
233        let mut uvars = Vec::new();
234        let mut sub = self.shifted();
235        for uvar in &ct.uvars {
236            uvars.push(sub.bounded_tyvar(uvar)?);
237            sub.bshift(1);
238            sub.rbshift(1);
239        }
240        let imports = ct
241            .imports
242            .iter()
243            .map(|ed| sub.extern_decl(ed).map_err(Into::into))
244            .collect::<Result<Vec<ExternDecl<'a>>, Self::Error>>()?;
245        let instance = sub.qualified_instance(&ct.instance)?;
246        Ok(Component {
247            uvars,
248            imports,
249            instance,
250        })
251    }
252}
253
254/// A substitution that shifts bound variables up by a defined offset.
255/// This will generally be accessed through [`Shifted`] below.  It is
256/// important to ensure that a bound variable produced by a
257/// substitution is not captured.
258struct RBShift {
259    rbshift: i32,
260}
261impl<'a> Shiftable<'a> for RBShift {
262    type Inner = Self;
263    fn shifted<'b>(&'b self) -> Shifted<'b, Self::Inner> {
264        Shifted::new(self)
265    }
266}
267impl<'a> Substitution<'a> for RBShift {
268    type Error = Void;
269    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
270        Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Bound(
271            i.checked_add_signed(self.rbshift).unwrap(),
272        )))))
273    }
274    fn subst_evar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
275        Ok(None)
276    }
277    fn subst_uvar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
278        Ok(None)
279    }
280}
281
282/// A substitution that can be converted into a [`Shifted`]
283/// substitution. All types other than [`Shifted`] itself should
284/// implement this with the obvious option of
285/// ```
286/// impl<'a> Shiftable<'a> for A {
287///     type Inner = Self;
288///     fn shifted<'b>(&'b self) -> Shifted<'b, Self::Inner> { Shifted::new(self) }
289/// }
290/// ```
291/// Unfortunately, it is not reasonably possible to provide this
292/// automatically without specialization.
293pub trait Shiftable<'a> {
294    type Inner: ?Sized + Substitution<'a>;
295    fn shifted<'c>(&'c self) -> Shifted<'c, Self::Inner>;
296}
297
298/// A "shifted" version of a substitution, used internally to assure
299/// that substitution is capture-avoiding.
300pub struct Shifted<'b, A: ?Sized> {
301    /// The substitution which is being shifted
302    underlying: &'b A,
303    /// The offset to apply to bound variables before querying the
304    /// original substitution
305    bshift: i32,
306    /// The offset to apply to outer instance indices before
307    /// querying the original substitution
308    oshift: i32,
309    /// The offset to apply to free evar indices before
310    /// querying the original substitution
311    eshift: i32,
312    /// The offset to apply to free uvar indices before
313    /// querying the original substitution
314    ushift: i32,
315    /// The offset to apply to bound variables in the result of the
316    /// original substitution
317    rbshift: i32,
318}
319impl<'b, A: ?Sized> Clone for Shifted<'b, A> {
320    fn clone(&self) -> Self {
321        Self {
322            underlying: self.underlying,
323            bshift: self.bshift,
324            oshift: self.oshift,
325            eshift: self.eshift,
326            ushift: self.ushift,
327            rbshift: self.rbshift,
328        }
329    }
330}
331impl<'a, 'b, A: ?Sized + Substitution<'a>> Shiftable<'a> for Shifted<'b, A> {
332    type Inner = A;
333    fn shifted<'c>(&'c self) -> Shifted<'c, Self::Inner> {
334        self.clone()
335    }
336}
337
338impl<'a, 'b, A: ?Sized + Substitution<'a>> Shifted<'b, A> {
339    fn new(s: &'b A) -> Self {
340        Self {
341            underlying: s,
342            bshift: 0,
343            oshift: 0,
344            eshift: 0,
345            ushift: 0,
346            rbshift: 0,
347        }
348    }
349    fn bshift(&mut self, bshift: i32) {
350        self.bshift += bshift;
351    }
352    #[allow(unused)]
353    fn oshift(&mut self, oshift: i32) {
354        self.oshift += oshift;
355    }
356    #[allow(unused)]
357    fn ushift(&mut self, ushift: i32) {
358        self.ushift += ushift;
359    }
360    #[allow(unused)]
361    fn eshift(&mut self, eshift: i32) {
362        self.eshift += eshift;
363    }
364    fn rbshift(&mut self, rbshift: i32) {
365        self.rbshift += rbshift;
366    }
367
368    fn sub_rbshift(
369        &self,
370        dt: Result<Option<Defined<'a>>, <Self as Substitution<'a>>::Error>,
371    ) -> Result<Option<Defined<'a>>, <Self as Substitution<'a>>::Error> {
372        match dt {
373            Ok(Some(dt)) => {
374                let rbsub = RBShift {
375                    rbshift: self.rbshift,
376                };
377                Ok(Some(rbsub.defined(&dt).not_void()))
378            }
379            _ => dt,
380        }
381    }
382}
383
384impl<'a, 'b, A: ?Sized + Substitution<'a>> Substitution<'a> for Shifted<'b, A> {
385    type Error = A::Error;
386    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
387        match i.checked_add_signed(-self.bshift) {
388            Some(i) => self.sub_rbshift(self.underlying.subst_bvar(i)),
389            _ => Ok(None),
390        }
391    }
392    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
393        match (
394            o.checked_add_signed(-self.oshift),
395            i.checked_add_signed(-self.eshift),
396        ) {
397            (Some(o), Some(i)) => self.sub_rbshift(self.underlying.subst_evar(o, i)),
398            _ => Ok(None),
399        }
400    }
401    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
402        match (
403            o.checked_add_signed(-self.oshift),
404            i.checked_add_signed(-self.ushift),
405        ) {
406            (Some(o), Some(i)) => self.sub_rbshift(self.underlying.subst_uvar(o, i)),
407            _ => Ok(None),
408        }
409    }
410}
411
412/// Innerizing can fail because a type variable needs to be taken
413/// through an `outer_boundary` but cannot be resolved to a concrete
414/// type that can be copied.
415#[derive(Debug)]
416pub enum InnerizeError {
417    IndefiniteTyvar,
418}
419/// An innerize substitution is used to bring an outer type alias
420/// inwards through one context.
421pub struct Innerize<'c, 'p, 'a> {
422    /// What ctx was this type originally in?
423    ctx: &'c Ctx<'p, 'a>,
424    /// Are we crossing an outer_boundary?
425    outer_boundary: bool,
426}
427impl<'c, 'p, 'a> Shiftable<'a> for Innerize<'c, 'p, 'a> {
428    type Inner = Self;
429    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
430        Shifted::new(self)
431    }
432}
433impl<'c, 'p, 'a> Substitution<'a> for Innerize<'c, 'p, 'a> {
434    type Error = InnerizeError;
435    fn subst_bvar(&self, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
436        Ok(None)
437    }
438    // Note that even if the variables resolve, what they resolve to
439    // needs to itself be innerized, since it was also designed for
440    // this context.
441    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
442        if !self.outer_boundary {
443            Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Free(
444                FreeTyvar::E(o + 1, i),
445            )))))
446        } else {
447            match self.ctx.resolve_tyvar(&Tyvar::Free(FreeTyvar::E(o, i))) {
448                ResolvedTyvar::Definite(dt) => Ok(Some(self.defined(&dt)?)),
449                _ => Err(InnerizeError::IndefiniteTyvar),
450            }
451        }
452    }
453    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
454        if !self.outer_boundary {
455            Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Free(
456                FreeTyvar::U(o + 1, i),
457            )))))
458        } else {
459            match self.ctx.resolve_tyvar(&Tyvar::Free(FreeTyvar::U(o, i))) {
460                ResolvedTyvar::Definite(dt) => Ok(Some(self.defined(&dt)?)),
461                _ => Err(InnerizeError::IndefiniteTyvar),
462            }
463        }
464    }
465}
466impl<'c, 'p, 'a> Innerize<'c, 'p, 'a> {
467    pub fn new(ctx: &'c Ctx<'p, 'a>, outer_boundary: bool) -> Innerize<'c, 'p, 'a> {
468        Innerize {
469            ctx,
470            outer_boundary,
471        }
472    }
473}
474
475/// The empty (void) type
476pub enum Void {}
477
478/// Things that you can call [`not_void`](Unvoidable::not_void) on
479pub trait Unvoidable {
480    type Result;
481    fn not_void(self) -> Self::Result;
482}
483
484/// Eliminate a Result<_, Void>
485impl<A> Unvoidable for Result<A, Void> {
486    type Result = A;
487    fn not_void(self) -> A {
488        match self {
489            Ok(x) => x,
490            Err(v) => match v {},
491        }
492    }
493}
494
495/// An opening substitution is used to map bound variables into
496/// free variables. Note that because of the differences in ordering
497/// for bound variable indices (inside out) and context variables
498/// (left to right, but variables are inserted in outside-in order),
499/// `Bound(0)` gets mapped to `Free(0, base + n)`.
500pub struct Opening {
501    /// Whether to produce E or U free variables
502    is_universal: bool,
503    /// At what index in the context are the free variables being
504    /// inserted?
505    free_base: u32,
506    /// How many bound variables are being shifted to the context
507    how_many: u32,
508}
509impl<'a> Shiftable<'a> for Opening {
510    type Inner = Self;
511    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
512        Shifted::new(self)
513    }
514}
515impl<'a> Substitution<'a> for Opening {
516    type Error = Void;
517    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Void> {
518        let mk = |i| {
519            let fi = self.free_base + self.how_many - i - 1;
520            if self.is_universal {
521                FreeTyvar::U(0, fi)
522            } else {
523                FreeTyvar::E(0, fi)
524            }
525        };
526        Ok(if i < self.how_many {
527            Some(Defined::Handleable(Handleable::Var(Tyvar::Free(mk(i)))))
528        } else {
529            None
530        })
531    }
532    fn subst_evar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Void> {
533        Ok(None)
534    }
535    fn subst_uvar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Void> {
536        Ok(None)
537    }
538}
539impl Opening {
540    pub fn new(is_universal: bool, free_base: u32) -> Self {
541        Opening {
542            is_universal,
543            free_base,
544            how_many: 0,
545        }
546    }
547    pub fn next(&mut self) {
548        self.how_many += 1;
549    }
550}
551
552/// A closing substitution is used to map free variables into bound
553/// variables when converting a type being built in a context to a
554/// closed(ish) type that is above that context.
555///
556/// Like [`Opening`], a given [`Closing`] substitution either affects
557/// only existential variables or affects only universal variables, as
558/// these are closed at different times.
559pub struct Closing {
560    /// If this substitution applies to universal variables, this
561    /// keeps track of which ones are imported and which are
562    /// not. Non-imported universal variables may not be referred to
563    /// in types.
564    ///
565    /// Invariant: If this is provided, its length must be equal to
566    /// self.how_many
567    universal_imported: Option<Vec<bool>>,
568    /// How many of the relevant (u/e) free vars are valid at this point.
569    how_many: u32,
570}
571impl Closing {
572    pub fn new(is_universal: bool) -> Self {
573        let universal_imported = if is_universal { Some(Vec::new()) } else { None };
574        Closing {
575            universal_imported,
576            how_many: 0,
577        }
578    }
579    fn is_universal(&self) -> bool {
580        self.universal_imported.is_some()
581    }
582    pub fn next_u(&mut self, imported: bool) {
583        let Some(ref mut importeds) = self.universal_imported else {
584            panic!("next_u called on existential Closing");
585        };
586        importeds.push(imported);
587        self.how_many += 1;
588    }
589    pub fn next_e(&mut self) {
590        if self.is_universal() {
591            panic!("next_e called on universal Closing");
592        };
593        self.how_many += 1;
594    }
595    fn subst_uevar<'a>(
596        &self,
597        ue_is_u: bool,
598        o: u32,
599        i: u32,
600    ) -> Result<Option<Defined<'a>>, ClosingError> {
601        if self.is_universal() ^ ue_is_u {
602            return Ok(None);
603        }
604        let mk_ue = |o, i| {
605            if self.is_universal() {
606                Tyvar::Free(FreeTyvar::U(o, i))
607            } else {
608                Tyvar::Free(FreeTyvar::E(o, i))
609            }
610        };
611        let mk = |v| Ok(Some(Defined::Handleable(Handleable::Var(v))));
612        if o > 0 {
613            return mk(mk_ue(o - 1, i));
614        }
615        if i >= self.how_many {
616            return Err(ClosingError::UnknownVar(false, i));
617        }
618        let bidx = if let Some(imported) = &self.universal_imported {
619            if !imported[i as usize] {
620                return Err(ClosingError::UnimportedVar(i));
621            }
622            imported[i as usize..].iter().filter(|x| **x).count() as u32 - 1
623        } else {
624            self.how_many - i - 1
625        };
626        mk(Tyvar::Bound(bidx))
627    }
628}
629impl<'a> Shiftable<'a> for Closing {
630    type Inner = Self;
631    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
632        Shifted::new(self)
633    }
634}
635/// Closing can fail for a few reasons:
636#[derive(Debug)]
637#[allow(unused)]
638pub enum ClosingError {
639    /// A variable was encountered that isn't currently being moved to
640    /// a bound variable. This is an internal invariant violation in
641    /// the typechecker, not an issue of a malformed input type.
642    UnknownVar(bool, u32),
643    /// A universal variable wasn't imported. This is probably an
644    /// internal invariant violation in the typechecker.
645    UnimportedVar(u32),
646}
647impl<'a> Substitution<'a> for Closing {
648    type Error = ClosingError;
649    fn subst_bvar(&self, _: u32) -> Result<Option<Defined<'a>>, ClosingError> {
650        Ok(None)
651    }
652    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, ClosingError> {
653        self.subst_uevar(false, o, i)
654    }
655    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, ClosingError> {
656        self.subst_uevar(true, o, i)
657    }
658}