insert a test that we detect huge terms

Author: nikomatsakis

crates/formality-prove/src/program.rs

@@ -14,6 +14,9 @@ pub struct Program {
 }
 
 impl Program {
+    /// Max size used in unit tests that are not stress testing maximum size.
+    pub const DEFAULT_MAX_SIZE: usize = 222;
+
     pub fn impl_decls<'s>(&'s self, trait_id: &'s TraitId) -> impl Iterator<Item = &'s ImplDecl> {
         self.impl_decls
             .iter()

crates/formality-prove/src/prove.rs

@@ -13,8 +13,10 @@ use formality_types::{
     cast::Upcast,
     collections::Set,
     grammar::{Binder, Wcs},
+    set,
     visit::Visit,
 };
+use tracing::Level;
 
 use crate::program::Program;
 
@@ -30,7 +32,19 @@ pub fn prove(
     let assumptions: Wcs = assumptions.upcast();
     let goal: Wcs = goal.upcast();
 
-    let fv_in = (&assumptions, &goal).free_variables();
+    let span = tracing::span!(Level::DEBUG, "prove", ?goal, ?assumptions);
+    let _guard = span.enter();
+
+    let term_in = (&assumptions, &goal);
+    let fv_in = term_in.free_variables();
+    if term_in.size() > program.max_size {
+        tracing::debug!(
+            "term has size {} which exceeds max size of {}",
+            term_in.size(),
+            program.max_size
+        );
+        return set![Binder::dummy(Constraints::default().ambiguous())];
+    }
 
     let cs = prove_wc_list(program, assumptions, goal);
 
@@ -39,5 +53,7 @@ pub fn prove(
         .iter()
         .for_each(|fv| assert!(fv_in.contains(&fv)));
 
+    tracing::debug!(?cs);
+
     cs
 }

crates/formality-prove/src/test.rs

@@ -11,6 +11,7 @@ use crate::{
 
 mod eq_partial_eq;
 mod exists_constraints;
+mod expanding;
 mod occurs_check;
 mod simple_impl;
 mod universes;

crates/formality-prove/src/test/eq_partial_eq.rs

@@ -10,7 +10,7 @@ use crate::{program::Program, prove::prove};
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
     Program {
-        max_size: 22,
+        max_size: Program::DEFAULT_MAX_SIZE,
         trait_decls: vec![
             term("trait Eq<ty Self> where {is_implemented(PartialEq(Self))}"),
             term("trait PartialEq<ty Self> where {}"),

crates/formality-prove/src/test/exists_constraints.rs

@@ -9,7 +9,7 @@ use super::test_prove;
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
     Program {
-        max_size: 22,
+        max_size: Program::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Foo<ty Self> where {}")],
         impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
         alias_eq_decls: vec![],

crates/formality-prove/src/test/expanding.rs

@@ -0,0 +1,30 @@
+use expect_test::expect;
+use formality_macros::test;
+use formality_types::parse::term;
+
+use crate::program::Program;
+
+/// Simple example program consisting only of two trait declarations.
+fn program() -> Program {
+    Program {
+        max_size: 10,
+        trait_decls: vec![term("trait Debug<ty Self> where {}")],
+        impl_decls: vec![term(
+            "impl<ty T> Debug(Vec<T>) where {is_implemented(Debug(T))}",
+        )],
+        alias_eq_decls: vec![],
+        alias_bound_decls: vec![],
+    }
+}
+
+/// There is no U that is equal to all T.
+#[test]
+fn expanding() {
+    let constraints = super::test_prove(program(), term("<ty T> ({}, {is_implemented(Debug(T))})"));
+    expect![[r#"
+        {
+            <> Constraints { known_true: false, substitution: Substitution { map: {} } },
+        }
+    "#]]
+    .assert_debug_eq(&constraints);
+}

crates/formality-prove/src/test/occurs_check.rs

@@ -9,7 +9,7 @@ use super::test_prove;
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
     Program {
-        max_size: 22,
+        max_size: Program::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Foo<ty Self> where {}")],
         impl_decls: vec![term("impl<ty T> Foo(Vec<T>) where {}")],
         alias_eq_decls: vec![],

crates/formality-prove/src/test/simple_impl.rs

@@ -10,7 +10,7 @@ use crate::{program::Program, prove::prove};
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
     Program {
-        max_size: 22,
+        max_size: Program::DEFAULT_MAX_SIZE,
         trait_decls: vec![term("trait Debug<ty Self> where {}")],
         impl_decls: vec![
             term("impl<ty T> Debug(Vec<T>) where {is_implemented(Debug(T))}"),

crates/formality-prove/src/test/universes.rs

@@ -7,7 +7,7 @@ use crate::program::Program;
 /// Simple example program consisting only of two trait declarations.
 fn program() -> Program {
     Program {
-        max_size: 22,
+        max_size: Program::DEFAULT_MAX_SIZE,
         trait_decls: vec![],
         impl_decls: vec![],
         alias_eq_decls: vec![],