From a3205cfa58fb3cf16757c65345dd99d27e73a42f Mon Sep 17 00:00:00 2001 From: tslil Date: Mon, 27 Apr 2026 10:13:10 +0100 Subject: add distinction between hypothetical and concrete elements to the set checker, it now enforces that all arms in case are well typed! --- src/checker.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/checker.rs') 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 { .. } => { -- cgit v1.3.1