add distinction between hypothetical and concrete elements to the set checker, it now enforces that all arms in case are well typed!

1 files changed, 7 insertions, 2 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 3ebcb4d..1760c0e 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -1,5 +1,5 @@
 use crate::ast::*;
-use crate::checker_state::{CheckerError, CheckerState};
+use crate::checker_state::{CheckerError, CheckerState, ElementValue};
 
 use tracing::{debug, instrument};
 
@@ -25,7 +25,12 @@ impl CheckerState {
 
                 Decl::Element { name, element, set } => {
                     let set = self.check_set(set)?;
-                    let element = self.check_element(element, &set)?;
+                    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)
                 }
                 Decl::Signature { .. } => {