rework checking logic to revolve around "stuck" computations, the meaning of Hypothetical is now reserved for formal bindings

1 files changed, 2 insertions, 7 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 05ebca2..976b9fb 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -1,5 +1,5 @@
 use crate::ast::*;
-use crate::checker_state::{CheckerError, CheckerState, ElementValue};
+use crate::checker_state::{CheckerError, CheckerState};
 
 use tracing::{debug, instrument};
 
@@ -26,12 +26,7 @@ impl CheckerState {
                 Decl::Element { name, element, set } => {
                     let set = self.check_set(set.clone())?;
                     let element = self.check_element(element.clone().into(), &set)?;
-                    if matches!(element, ElementValue::Hypothetical(_)) {
-                        panic!(
-                            "invariant violation: from concrete values at the top level we returned a hypothetical value"
-                        );
-                    }
-                    self.add_element(name.clone(), element, set)
+                    self.add_element(name.clone(), element.into(), set)
                 }
                 Decl::Signature { name, signature } => {
                     let signature = self.check_signature(signature.clone())?;