add a size method to Visitor

this can be used to force ambiguity

Author: nikomatsakis

crates/formality-macros/src/visit.rs

@@ -9,6 +9,8 @@ pub(crate) fn derive_visit(mut s: synstructure::Structure) -> TokenStream {
 
     let free_variables_body = s.each(|field| quote!(output.extend(Visit::free_variables(#field))));
 
+    let size_body = s.each(|field| quote!(__sum += Visit::size(#field)));
+
     // s.add_bounds(synstructure::AddBounds::None);
     s.gen_impl(quote! {
         use crate::derive_links::{Visit, Variable};
@@ -21,6 +23,15 @@ pub(crate) fn derive_visit(mut s: synstructure::Structure) -> TokenStream {
                 }
                 output
             }
+
+            fn size(&self) -> usize {
+                let mut __sum = 0;
+                __sum += 1;
+                match self {
+                    #size_body
+                }
+                __sum
+            }
         }
     })
 }

crates/formality-prove/src/prove/constraints.rs

@@ -136,7 +136,19 @@ impl Fold for Constraints {
 
 impl Visit for Constraints {
     fn free_variables(&self) -> Vec<Variable> {
-        self.substitution.free_variables()
+        let Constraints {
+            known_true: _,
+            substitution,
+        } = self;
+        substitution.free_variables()
+    }
+
+    fn size(&self) -> usize {
+        let Constraints {
+            known_true: _,
+            substitution,
+        } = self;
+        substitution.size()
     }
 }
 

crates/formality-rust/src/trait_binder.rs

@@ -48,6 +48,10 @@ where
     fn free_variables(&self) -> Vec<formality_types::grammar::Variable> {
         self.explicit_binder.free_variables()
     }
+
+    fn size(&self) -> usize {
+        self.explicit_binder.size()
+    }
 }
 
 impl<T> Fold for TraitBinder<T>

crates/formality-types/src/grammar/binder.rs

@@ -173,6 +173,10 @@ impl<T: Visit> Visit for Binder<T> {
     fn free_variables(&self) -> Vec<Variable> {
         self.term.free_variables()
     }
+
+    fn size(&self) -> usize {
+        self.term.size()
+    }
 }
 
 impl<T: Fold> Fold for Binder<T> {

crates/formality-types/src/grammar/ids.rs

@@ -32,6 +32,10 @@ macro_rules! id {
                 fn free_variables(&self) -> Vec<Variable> {
                     vec![]
                 }
+
+                fn size(&self) -> usize {
+                    1
+                }
             }
 
             impl Fold for $n {

crates/formality-types/src/grammar/ty.rs

@@ -143,6 +143,10 @@ impl Visit for InferenceVar {
     fn free_variables(&self) -> Vec<Variable> {
         vec![self.upcast()]
     }
+
+    fn size(&self) -> usize {
+        1
+    }
 }
 
 #[term((rigid $name $*parameters))]
@@ -397,6 +401,28 @@ impl UpcastFrom<LtData> for LtData {
     }
 }
 
+impl Visit for LtData {
+    fn free_variables(&self) -> Vec<Variable> {
+        match self {
+            LtData::Variable(v) => {
+                if v.is_free() {
+                    vec![v.clone()]
+                } else {
+                    vec![]
+                }
+            }
+            LtData::Static => vec![],
+        }
+    }
+
+    fn size(&self) -> usize {
+        match self {
+            LtData::Variable(v) => v.size(),
+            LtData::Static => 1,
+        }
+    }
+}
+
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub enum Variable {
     PlaceholderVar(PlaceholderVar),
@@ -489,6 +515,10 @@ impl Visit for Variable {
             vec![]
         }
     }
+
+    fn size(&self) -> usize {
+        1
+    }
 }
 
 impl UpcastFrom<Variable> for Parameter {
@@ -670,6 +700,10 @@ impl Visit for Substitution {
         v.extend(self.domain());
         v
     }
+
+    fn size(&self) -> usize {
+        self.range().iter().map(|r| r.size()).sum()
+    }
 }
 
 /// A substitution that is only between variables.

crates/formality-types/src/visit.rs

@@ -2,7 +2,7 @@ use std::sync::Arc;
 
 use crate::{
     collections::Set,
-    grammar::{Lt, LtData, Parameter, Ty, Universe, Variable},
+    grammar::{Lt, Parameter, Ty, Universe, Variable},
 };
 
 /// Invoked for each variable that we find when Visiting, ignoring variables bound by binders
@@ -17,6 +17,10 @@ pub trait Visit: Sized {
     /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important).
     fn free_variables(&self) -> Vec<Variable>;
 
+    /// Measures the overall size of the term by counting constructors etc.
+    /// Used to determine overflow.
+    fn size(&self) -> usize;
+
     /// True if this term references only placeholder variables.
     /// This means that it contains no inference variables.
     /// If this is a goal, then when we prove it true, we don't expect any substitution.
@@ -49,57 +53,80 @@ impl<T: Visit> Visit for Vec<T> {
     fn free_variables(&self) -> Vec<Variable> {
         self.iter().flat_map(|e| e.free_variables()).collect()
     }
+
+    fn size(&self) -> usize {
+        self.iter().map(|e| e.size()).sum()
+    }
 }
 
 impl<T: Visit + Ord> Visit for Set<T> {
     fn free_variables(&self) -> Vec<Variable> {
         self.iter().flat_map(|e| e.free_variables()).collect()
     }
+
+    fn size(&self) -> usize {
+        self.iter().map(|e| e.size()).sum()
+    }
 }
 
 impl<T: Visit> Visit for Option<T> {
     fn free_variables(&self) -> Vec<Variable> {
         self.iter().flat_map(|e| e.free_variables()).collect()
     }
+
+    fn size(&self) -> usize {
+        self.as_ref().map(|e| e.size()).unwrap_or(0)
+    }
 }
 
 impl<T: Visit> Visit for Arc<T> {
     fn free_variables(&self) -> Vec<Variable> {
         T::free_variables(self)
     }
+
+    fn size(&self) -> usize {
+        T::size(self)
+    }
 }
 
 impl Visit for Ty {
     fn free_variables(&self) -> Vec<Variable> {
         self.data().free_variables()
     }
+
+    fn size(&self) -> usize {
+        self.data().size()
+    }
 }
 
 impl Visit for Lt {
     fn free_variables(&self) -> Vec<Variable> {
-        match self.data() {
-            LtData::Variable(v) => {
-                if v.is_free() {
-                    vec![v.clone()]
-                } else {
-                    vec![]
-                }
-            }
-            LtData::Static => vec![],
-        }
+        self.data().free_variables()
+    }
+
+    fn size(&self) -> usize {
+        self.data().size()
     }
 }
 
 impl Visit for usize {
     fn free_variables(&self) -> Vec<Variable> {
         vec![]
     }
+
+    fn size(&self) -> usize {
+        1
+    }
 }
 
 impl Visit for u32 {
     fn free_variables(&self) -> Vec<Variable> {
         vec![]
     }
+
+    fn size(&self) -> usize {
+        1
+    }
 }
 
 impl<A: Visit, B: Visit> Visit for (A, B) {
@@ -110,6 +137,11 @@ impl<A: Visit, B: Visit> Visit for (A, B) {
         fv.extend(b.free_variables());
         fv
     }
+
+    fn size(&self) -> usize {
+        let (a, b) = self;
+        a.size() + b.size()
+    }
 }
 
 impl<A: Visit, B: Visit, C: Visit> Visit for (A, B, C) {
@@ -121,10 +153,19 @@ impl<A: Visit, B: Visit, C: Visit> Visit for (A, B, C) {
         fv.extend(c.free_variables());
         fv
     }
+
+    fn size(&self) -> usize {
+        let (a, b, c) = self;
+        a.size() + b.size() + c.size()
+    }
 }
 
 impl<A: Visit> Visit for &A {
     fn free_variables(&self) -> Vec<Variable> {
         A::free_variables(self)
     }
+
+    fn size(&self) -> usize {
+        A::size(self)
+    }
 }