Cherry-picked prove_sub to use Wcs::all_sub

Author: tiif

crates/formality-prove/src/prove.rs

@@ -7,6 +7,7 @@ mod negation;
 mod prove_after;
 mod prove_eq;
 pub mod prove_normalize;
+mod prove_sub;
 mod prove_via;
 mod prove_wc;
 mod prove_wc_list;

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

@@ -0,0 +1,55 @@
+use formality_core::judgment_fn;
+use formality_types::grammar::{Parameter, Relation, RigidTy, TyData, Wcs};
+
+use crate::{
+    decls::Decls,
+    prove::{prove, prove_after::prove_after, prove_normalize::prove_normalize},
+};
+
+use super::{constraints::Constraints, env::Env};
+
+judgment_fn! {
+    pub fn prove_sub(
+        _decls: Decls,
+        env: Env,
+        assumptions: Wcs,
+        a: Parameter,
+        b: Parameter,
+    ) => Constraints {
+        debug(a, b, assumptions, env)
+
+        assert(a.kind() == b.kind())
+
+        trivial(a == b => Constraints::none(env))
+
+        (
+            (prove_normalize(&decls, env, &assumptions, &x) => (c, y))
+            (prove_after(&decls, c, &assumptions, Relation::sub(y, &z)) => c)
+            ----------------------------- ("normalize-l")
+            (prove_sub(decls, env, assumptions, x, z) => c)
+        )
+
+        (
+            (prove_normalize(&decls, env, &assumptions, &y) => (c, z))
+            (prove_after(&decls, c, &assumptions, Relation::sub(&x, &z)) => c)
+            ----------------------------- ("normalize-r")
+            (prove_sub(decls, env, assumptions, x, y) => c)
+        )
+
+        (
+            (let RigidTy { name: a_name, parameters: a_parameters } = a)
+            (let RigidTy { name: b_name, parameters: b_parameters } = b)
+            (if a_name == b_name)!
+            (prove(decls, env, assumptions, Wcs::all_sub(a_parameters, b_parameters)) => c)
+            ----------------------------- ("rigid")
+            (prove_sub(decls, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c)
+        )
+
+        // FIXME: uncomment this when adding prove_outlives
+        //(
+        //    (prove_outlives(decls, env, assumptions, a, b) => c)
+        //    ----------------------------- ("lifetime => outlives")
+        //    (prove_sub(decls, env, assumptions, a: Lt, b: Lt) => c)
+        //)
+    }
+}

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

@@ -10,13 +10,13 @@ use crate::{
         prove,
         prove_after::prove_after,
         prove_eq::prove_eq,
+        prove_sub::prove_sub,
         prove_via::prove_via,
         prove_wf::prove_wf,
     },
 };
 
 use super::constraints::Constraints;
-use formality_types::grammar::Parameter::Ty;
 
 judgment_fn! {
     /// The "heart" of the trait system -- prove that a where-clause holds given a set of declarations, variable environment, and set of assumptions.
@@ -56,15 +56,6 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c)
         )
 
-        // FIXME: improve the subtype rule after adding lifetime
-        (
-            (if let Ty(_) = param1.clone())!
-            (if let Ty(_) = param2.clone())!
-            (if param1 == param2)!
-            ----------------------------- ("subtype - reflexive")
-            (prove_wc(_decls, env, _assumptions, WcData::Relation(Relation::Sub(param1, param2))) => Constraints::none(env))
-        )
-
         (
             (decls.impl_decls(&trait_ref.trait_id) => i)!
             (let (env, subst) = env.existential_substitution(&i.binder))
@@ -117,6 +108,12 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Relation::Equals(a, b)) => c)
         )
 
+        (
+            (prove_sub(decls, env, assumptions, a, b) => c)
+            ----------------------------- ("subtype")
+            (prove_wc(decls, env, assumptions, WcData::Relation(Relation::Sub(a, b))) => c)
+        )
+
         (
             (for_all(&decls, &env, &assumptions, &trait_ref.parameters, &prove_wf) => c)
             (let t = decls.trait_decl(&trait_ref.trait_id))

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

@@ -28,6 +28,20 @@ impl Wcs {
             .upcasted()
             .collect()
     }
+
+    /// Goal(s) to prove `a` and `b` are subtypes.
+    ///
+    /// FIXME: This should take variance into account.
+    pub fn all_sub(a: impl Upcast<Vec<Parameter>>, b: impl Upcast<Vec<Parameter>>) -> Wcs {
+        let a: Vec<Parameter> = a.upcast();
+        let b: Vec<Parameter> = b.upcast();
+        assert_eq!(a.len(), b.len());
+        a.into_iter()
+            .zip(b)
+            .map(|(a, b)| Relation::sub(a, b))
+            .upcasted()
+            .collect()
+    }
 }
 
 impl<'w> IntoIterator for &'w Wcs {