Improve check error message and document query-based semantics for constructor terms

src/ast/mod.rs

@@ -849,7 +849,14 @@ where
     PrintOverallStatistics(Span, Option<String>),
     /// The `check` command checks that the given facts
     /// match at least once in the current database.
-    /// The list of facts is matched in the same way a [`Command::Rule`] is matched.
+    /// The list of facts is matched in the same way a [`Command::Rule`] is matched,
+    /// i.e., it runs a query against the current e-graph state.
+    ///
+    /// Note: For `eqsort` terms (e.g., constructor applications like `(Num 6)`),
+    /// the terms must already be present in the e-graph for the check to succeed.
+    /// Unlike primitive types (e.g., `i64`), constructor terms are not automatically
+    /// materialized by `check`. This mirrors the behavior of rules, which also only
+    /// match against existing e-graph state.
     ///
     /// Example:
     ///
@@ -867,6 +874,16 @@ where
     /// [ERROR] Check failed
     /// [INFO ] Command failed as expected.
     /// ```
+    ///
+    /// Example using constructor terms (terms must be in the e-graph first):
+    ///
+    /// ```text
+    /// (datatype Math)
+    /// (constructor Num (i64) Math)
+    /// (let x (Num 6))
+    /// (check (= x (Num 6)))       ;; succeeds: (Num 6) is now in the e-graph
+    /// (fail (check (= (Num 7) (Num 7))))  ;; fails: (Num 7) is not in the e-graph
+    /// ```
     Check(Span, Vec<GenericFact<Head, Leaf>>),
     Prove(Span, Vec<GenericFact<Head, Leaf>>),
     ProveExists(Span, Head),

src/lib.rs

@@ -2104,7 +2104,7 @@ pub enum Error {
     TypeError(#[from] TypeError),
     #[error("Errors:\n{}", ListDisplay(.0, "\n"))]
     TypeErrors(Vec<TypeError>),
-    #[error("{}\nCheck failed: \n{}", .1, ListDisplay(.0, "\n"))]
+    #[error("{}\nCheck failed (are the relevant terms present in the e-graph?): \n{}", .1, ListDisplay(.0, "\n"))]
     CheckError(Vec<Fact>, Span),
     #[error("{1}\nNo such ruleset: {0}")]
     NoSuchRuleset(String, Span),

tests/check-constructor-not-in-egraph.egg

@@ -0,0 +1,22 @@
+;; This test verifies that check fails when constructor terms are not in the e-graph.
+;; The `check` command runs a query against existing e-graph state, so constructor
+;; terms (eqsort terms) must already be present for a check to succeed.
+
+(datatype Math)
+(constructor Num (i64) Math)
+
+;; This check fails because (Num 6) is not in the e-graph yet
+(fail (check (= (Num 6) (Num 6))))
+
+;; Introduce (Num 6) into the e-graph using let
+(let x (Num 6))
+
+;; Now this succeeds because (Num 6) is in the e-graph
+(check (= x (Num 6)))
+
+;; Two variable references to the same constructor term are also equal
+(let y (Num 6))
+(check (= x y))
+
+;; This still fails because (Num 7) is not in the e-graph
+(fail (check (= (Num 7) (Num 7))))

tests/snapshots/files__shared_snapshot_check_constructor_not_in_egraph.snap

@@ -0,0 +1,6 @@
+---
+source: tests/files.rs
+assertion_line: 94
+expression: snapshot_content_across_treatments
+---
+((Num 1))