aboutsummaryrefslogtreecommitdiff
path: root/src/checker_set.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/checker_set.rs')
-rw-r--r--src/checker_set.rs30
1 files changed, 23 insertions, 7 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs
index f13f686..2f934e2 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -120,6 +120,17 @@ impl CheckerState {
}
Ok(element.clone().into())
}
+ Element::ClaimedElement(instance) => {
+ let instance = self.check_instance(
+ instance.as_ref(),
+ set.map(|s| Signature::FromSet(s.clone())).as_ref(),
+ )?;
+ if let Instance::ElementCoerce(element) = instance {
+ Ok(element)
+ } else {
+ Ok(Element::ClaimedElement(Box::new(instance)))
+ }
+ }
Element::Var(v) => {
let lookup = self.lookup_element(&v)?;
@@ -275,12 +286,13 @@ impl CheckerState {
match inner {
// We're stuck on something that bottoms out in a binding
// blocking computation, nothing to be done here
- Element::Var(_) | Element::Project { .. } | Element::Case { .. } => {
- Ok(Element::Project {
- element: Box::new(inner),
- field: field.clone(),
- })
- }
+ Element::Var(_)
+ | Element::Project { .. }
+ | Element::Case { .. }
+ | Element::ClaimedElement(_) => Ok(Element::Project {
+ element: Box::new(inner),
+ field: field.clone(),
+ }),
Element::Record(assignations) => {
let sub_element = assignations
.into_iter()
@@ -382,7 +394,10 @@ impl CheckerState {
} => Some((field.clone(), *inner.clone())),
// These are all the cases which could become stuck on a
// formal binding
- Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None,
+ Element::Var(_)
+ | Element::Project { .. }
+ | Element::Case { .. }
+ | Element::ClaimedElement(_) => None,
Element::Literal(_) | Element::Record(_) => panic!(
"invariant violation: scrutinee is a non-variant value at variant set"
),
@@ -394,6 +409,7 @@ impl CheckerState {
let posit_equality_with = match &scrutinee {
Element::Var(v) => Some(v.clone()),
Element::Inject { .. }
+ | Element::ClaimedElement(_)
| Element::Project { .. }
| Element::Case { .. }
| Element::Literal(_)