hyperlight_component_util/
subtype.rs

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

hyperlight_component_util/
subtype.rs
