Prove ConstHasType predicates

Author: oli-obk

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

@@ -114,5 +114,12 @@ judgment_fn! {
             ----------------------------- ("trait ref is local")
             (prove_wc(decls, env, assumptions, Relation::WellFormed(p)) => c)
         )
+
+        (
+            (if ct.as_value().is_some())
+            (prove(decls, env, assumptions, Wcs::all_eq(vec![ct.as_value().unwrap().1], vec![ty])) => c)
+            ----------------------------- ("const has ty")
+            (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c)
+        )
     }
 }

crates/formality-rust/src/prove.rs

@@ -9,8 +9,8 @@ use formality_types::{
     cast::{To, Upcast, Upcasted},
     collections::Set,
     grammar::{
-        fresh_bound_var, AdtId, AliasTy, Binder, ParameterKind, Predicate, Relation, TraitId, Ty,
-        Wc, Wcs, PR,
+        fresh_bound_var, AdtId, AliasTy, Binder, ConstData, ParameterKind, Predicate, Relation,
+        TraitId, Ty, Wc, Wcs, PR,
     },
     seq,
 };
@@ -386,9 +386,12 @@ impl ToWcs for WhereClause {
                     .map(|wc| Wc::for_all(&vars, wc))
                     .collect()
             }
-            WhereClauseData::TypeOfConst(ct, ty) => {
-                Predicate::ConstHasType(ct.clone(), ty.clone()).upcast()
-            }
+            WhereClauseData::TypeOfConst(ct, ty) => match ct.data() {
+                // Concrete constants must have equal types
+                ConstData::Value(_, t) => Relation::eq(ty, t).upcast(),
+                // Generic constants must have where bounds constraining their type
+                ConstData::Variable(_) => Predicate::ConstHasType(ct.clone(), ty.clone()).upcast(),
+            },
         }
     }
 }

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

@@ -32,6 +32,13 @@ impl Const {
             ConstData::Variable(var) => Some(var.clone()),
         }
     }
+
+    pub fn as_value(&self) -> Option<(ValTree, Ty)> {
+        match self.data() {
+            ConstData::Value(v, t) => Some((v.clone(), t.clone())),
+            ConstData::Variable(_) => None,
+        }
+    }
 }
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]

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

@@ -93,6 +93,7 @@ pub enum Skeleton {
 impl Predicate {
     /// Separate an atomic predicate into the "skeleton" (which can be compared for equality using `==`)
     /// and the parameters (which must be related).
+    #[tracing::instrument(level = "trace", ret)]
     pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
         match self {
             Predicate::IsImplemented(TraitRef {
@@ -171,6 +172,7 @@ impl Relation {
         Self::Sub(p1.upcast(), p2.upcast())
     }
 
+    #[tracing::instrument(level = "trace", ret)]
     pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
         match self {
             Relation::Equals(a, b) => (Skeleton::Equals, vec![a.clone(), b.clone()]),

tests/consts.rs

@@ -23,11 +23,8 @@ fn test_ok() {
 #[test]
 fn test_holds() {
     expect_test::expect![[r#"
-        Err(
-            Error {
-                context: "check_trait_impl(impl <> Foo < const 0_(rigid (scalar bool)) > for (rigid (scalar u32)) where [] { })",
-                source: "failed to prove {Foo((rigid (scalar u32)), const 0_(rigid (scalar bool)))} given {}, got {}",
-            },
+        Ok(
+            (),
         )
     "#]]
     .assert_debug_eq(&test_program_ok(
@@ -61,3 +58,24 @@ fn test_mismatch() {
         ]",
     ));
 }
+
+#[test]
+fn test_generic_mismatch() {
+    expect_test::expect![[r#"
+        Err(
+            Error {
+                context: "check_trait_impl(impl <const> Foo < const ^const0_0 > for (rigid (scalar u32)) where [type_of_const ^const0_0 is (rigid (scalar u32))] { })",
+                source: "failed to prove {Foo((rigid (scalar u32)), const !const_1)} given {@ ConstHasType(!const_1 , (rigid (scalar u32)))}, got {}",
+            },
+        )
+    "#]]
+    .assert_debug_eq(&test_program_ok(
+        "[
+            crate Foo {
+                trait Foo<const C> where [type_of_const C is bool] {}
+
+                impl<const C> Foo<const C> for u32 where [type_of_const C is u32] {}
+            }
+        ]",
+    ));
+}