hyperlight_component_util/
subtype.rs

1// SPDX-License-Identifier: Apache-2.0
2// Copyright 2025 The Hyperlight Authors.
3
4use itertools::Itertools;
5
6use crate::etypes::{
7    Component, Ctx, Defined, Func, Handleable, Name, QualifiedInstance, ResourceId, TypeBound,
8    Tyvar, Value,
9};
10use crate::tv::ResolvedTyvar;
11
12/// The various ways in which a value can fail to be a subtype of another
13#[derive(Debug)]
14#[allow(dead_code)]
15pub enum Error<'r> {
16    /// An unnamed value that was expected was missing (e.g. in a
17    /// tuple or variant case)
18    MissingValue(Value<'r>),
19    /// A record field that was expected was missing
20    MissingRecordField(Name<'r>),
21    /// A variant case that was expected was missing
22    MissingVariantCase(Name<'r>),
23    /// A value type was present, but incompatible with its expected type
24    MismatchedValue(Value<'r>, Value<'r>),
25    /// A defined type was present, but incompatible with its expected type
26    MismatchedDefined(Box<Defined<'r>>, Box<Defined<'r>>),
27    /// A resource was present, but was not the same resource as was expected
28    MismatchedResources(ResourceId, ResourceId),
29    /// A type variable could not be resolved to be the same as the
30    /// expected one
31    MismatchedVars(Tyvar, Tyvar),
32    /// A resource was expected but a non-resource tyvar was found, or
33    /// vice versa
34    MismatchedResourceVar(Tyvar, ResourceId),
35    /// A handle was taken to something that wasn't a
36    /// resource. Strictly speaking, this might be a well-formedness
37    /// error on one side or the other rather than a subtyping error
38    NotResource(Handleable),
39}
40
41/// # Subtyping
42///
43/// Most of this is a very direct translation of the subset of the
44/// OCaml reference interpreter that we need here. Most of the bits
45/// with variables and instantiation that require being quite careful
46/// are not involved here, since during the elaboration that we are
47/// doing we never need to fully subtype entire component types, which
48/// makes this quite a bit simpler.
49impl<'p, 'a> Ctx<'p, 'a> {
50    pub fn subtype_value<'r>(
51        &self,
52        vt1: &'r Value<'a>,
53        vt2: &'r Value<'a>,
54    ) -> Result<(), Error<'a>> {
55        use Value::*;
56        use itertools::EitherOrBoth::*;
57        match (vt1, vt2) {
58            (Bool, Bool) => Ok(()),
59            (S(w1), S(w2)) if w1 == w2 => Ok(()),
60            (U(w1), U(w2)) if w1 == w2 => Ok(()),
61            (F(w1), F(w2)) if w1 == w2 => Ok(()),
62            (Char, Char) => Ok(()),
63            (String, String) => Ok(()),
64            (List(vt1), List(vt2)) => self.subtype_value(vt1, vt2),
65            (Record(rfs1), Record(rfs2)) => {
66                for rf2 in rfs2.iter() {
67                    match rfs1.iter().find(|rf| rf2.name.name == rf.name.name) {
68                        None => return Err(Error::MissingRecordField(rf2.name)),
69                        Some(rf1) => self.subtype_value(&rf1.ty, &rf2.ty)?,
70                    }
71                }
72                Ok(())
73            }
74            (Tuple(vts1), Tuple(vts2)) => {
75                vts1.iter()
76                    .zip_longest(vts2.iter())
77                    .try_for_each(|vs| match vs {
78                        Both(vt1, vt2) => self.subtype_value(vt1, vt2),
79                        Left(_) => Ok(()),
80                        Right(vt2) => Err(Error::MissingValue(vt2.clone())),
81                    })
82            }
83            (Flags(ns1), Flags(ns2)) => ns2
84                .iter()
85                .find(|n2| !ns1.iter().any(|n| n.name == n2.name))
86                .map_or(Ok(()), |n| Err(Error::MissingRecordField(*n))),
87            (Variant(vcs1), Variant(vcs2)) => {
88                for vc1 in vcs1.iter() {
89                    match vcs2.iter().find(|vc| vc1.name.name == vc.name.name) {
90                        None => return Err(Error::MissingVariantCase(vc1.name)),
91                        Some(vc2) => self.subtype_value_option(&vc1.ty, &vc2.ty)?,
92                    }
93                }
94                Ok(())
95            }
96            (Enum(ns1), Enum(ns2)) => ns1
97                .iter()
98                .find(|n1| !ns2.iter().any(|n| n.name == n1.name))
99                .map_or(Ok(()), |n| Err(Error::MissingVariantCase(*n))),
100            (Option(vt1), Option(vt2)) => self.subtype_value(vt1, vt2),
101            (Result(vt11, vt12), Result(vt21, vt22)) => self
102                .subtype_value_option(vt11, vt21)
103                .and(self.subtype_value_option(vt12, vt22)),
104            (Own(ht1), Own(ht2)) | (Borrow(ht1), Borrow(ht2)) => {
105                self.subtype_handleable_is_resource(ht1)?;
106                self.subtype_handleable_is_resource(ht2)?;
107                self.subtype_handleable(ht1, ht2)
108            }
109            (Var(_, vt1), vt2) => self.subtype_value(vt1, vt2),
110            (vt1, Var(_, vt2)) => self.subtype_value(vt1, vt2),
111            _ => Err(Error::MismatchedValue(vt1.clone(), vt2.clone())),
112        }
113    }
114    pub fn subtype_value_option<'r>(
115        &self,
116        vt1: &'r Option<Value<'a>>,
117        vt2: &'r Option<Value<'a>>,
118    ) -> Result<(), Error<'a>> {
119        match (vt1, vt2) {
120            (None, None) => Ok(()),
121            (None, Some(vt2)) => Err(Error::MissingValue(vt2.clone())),
122            (Some(_), None) => Ok(()),
123            (Some(vt1), Some(vt2)) => self.subtype_value(vt1, vt2),
124        }
125    }
126    pub fn subtype_var_var<'r>(&self, v1: &'r Tyvar, v2: &'r Tyvar) -> Result<(), Error<'a>> {
127        match (self.resolve_tyvar(v1), self.resolve_tyvar(v2)) {
128            (ResolvedTyvar::Definite(dt1), ResolvedTyvar::Definite(dt2)) => {
129                self.subtype_defined(&dt1, &dt2)
130            }
131            (ResolvedTyvar::E(o1, i1, _), ResolvedTyvar::E(o2, i2, _)) if o1 == o2 && i1 == i2 => {
132                Ok(())
133            }
134            (ResolvedTyvar::U(o1, i1, _), ResolvedTyvar::U(o2, i2, _)) if o1 == o2 && i1 == i2 => {
135                Ok(())
136            }
137            (ResolvedTyvar::Bound(_), _) | (_, ResolvedTyvar::Bound(_)) => {
138                panic!("internal invariant violation: stray bvar in subtype_var_var")
139            }
140            _ => Err(Error::MismatchedVars(v1.clone(), v2.clone())),
141        }
142    }
143    pub fn subtype_var_resource<'r>(
144        &self,
145        v1: &'r Tyvar,
146        rid2: &'r ResourceId,
147    ) -> Result<(), Error<'a>> {
148        match self.resolve_tyvar(v1) {
149            ResolvedTyvar::Definite(Defined::Handleable(Handleable::Resource(rid1)))
150                if rid1 == *rid2 =>
151            {
152                Ok(())
153            }
154            _ => Err(Error::MismatchedResourceVar(v1.clone(), *rid2)),
155        }
156    }
157    pub fn subtype_resource_var<'r>(
158        &self,
159        rid1: &'r ResourceId,
160        v2: &'r Tyvar,
161    ) -> Result<(), Error<'a>> {
162        match self.resolve_tyvar(v2) {
163            ResolvedTyvar::Definite(Defined::Handleable(Handleable::Resource(rid2)))
164                if *rid1 == rid2 =>
165            {
166                Ok(())
167            }
168            _ => Err(Error::MismatchedResourceVar(v2.clone(), *rid1)),
169        }
170    }
171    pub fn subtype_handleable<'r>(
172        &self,
173        ht1: &'r Handleable,
174        ht2: &'r Handleable,
175    ) -> Result<(), Error<'a>> {
176        match (ht1, ht2) {
177            (Handleable::Var(v1), Handleable::Var(v2)) => self.subtype_var_var(v1, v2),
178            (Handleable::Var(v1), Handleable::Resource(rid2)) => {
179                self.subtype_var_resource(v1, rid2)
180            }
181            (Handleable::Resource(rid1), Handleable::Var(v2)) => {
182                self.subtype_resource_var(rid1, v2)
183            }
184            (Handleable::Resource(rid1), Handleable::Resource(rid2)) => {
185                if rid1 == rid2 {
186                    Ok(())
187                } else {
188                    Err(Error::MismatchedResources(*rid1, *rid2))
189                }
190            }
191        }
192    }
193    pub fn subtype_func<'r>(
194        &self,
195        _ft1: &'r Func<'a>,
196        _ft2: &'r Func<'a>,
197    ) -> Result<(), Error<'a>> {
198        panic!("func <: func should be impossible to encounter during type elaboration")
199    }
200    pub fn subtype_qualified_instance<'r>(
201        &self,
202        _qi1: &'r QualifiedInstance<'a>,
203        _qi2: &'r QualifiedInstance<'a>,
204    ) -> Result<(), Error<'a>> {
205        panic!("qinstance <: qinstance should be impossible to encounter during type elaboration")
206    }
207    pub fn subtype_component<'r>(
208        &self,
209        _ct1: &'r Component<'a>,
210        _ct2: &'r Component<'a>,
211    ) -> Result<(), Error<'a>> {
212        panic!("component <: component should be impossible to encounter during type elaboration")
213    }
214    pub fn subtype_defined<'r>(
215        &self,
216        dt1: &'r Defined<'a>,
217        dt2: &'r Defined<'a>,
218    ) -> Result<(), Error<'a>> {
219        match (dt1, dt2) {
220            (Defined::Handleable(ht1), Defined::Handleable(ht2)) => {
221                self.subtype_handleable(ht1, ht2)
222            }
223            (Defined::Value(vt1), Defined::Value(vt2)) => self.subtype_value(vt1, vt2),
224            (Defined::Func(ft1), Defined::Func(ft2)) => self.subtype_func(ft1, ft2),
225            (Defined::Instance(it1), Defined::Instance(it2)) => {
226                self.subtype_qualified_instance(it1, it2)
227            }
228            (Defined::Component(ct1), Defined::Component(ct2)) => self.subtype_component(ct1, ct2),
229            _ => Err(Error::MismatchedDefined(
230                Box::new(dt1.clone()),
231                Box::new(dt2.clone()),
232            )),
233        }
234    }
235    pub fn subtype_handleable_is_resource<'r>(&self, ht: &'r Handleable) -> Result<(), Error<'a>> {
236        match ht {
237            Handleable::Resource(_) => Ok(()),
238            Handleable::Var(tv) => match self.resolve_tyvar(tv) {
239                ResolvedTyvar::Definite(Defined::Handleable(Handleable::Resource(_))) => Ok(()),
240                ResolvedTyvar::E(_, _, TypeBound::SubResource) => Ok(()),
241                ResolvedTyvar::U(_, _, TypeBound::SubResource) => Ok(()),
242                _ => Err(Error::NotResource(ht.clone())),
243            },
244        }
245    }
246}
hyperlight_component_util/subtype.rs

hyperlight_component_util/
subtype.rs
