add complete lifted sets

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(_)