Skip to content

Commit be4a0dd

Browse files
committed
Check that constants match their type
1 parent e5c943d commit be4a0dd

File tree

4 files changed

+93
-3
lines changed

4 files changed

+93
-3
lines changed

crates/formality-check/src/where_clauses.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ use formality_rust::{
66
};
77
use formality_types::{
88
cast::Upcast,
9-
grammar::{Fallible, Parameter, TraitRef},
9+
grammar::{ConstData, Fallible, Parameter, Relation, TraitRef},
1010
};
1111

1212
impl super::Check<'_> {
@@ -23,6 +23,7 @@ impl super::Check<'_> {
2323
}
2424

2525
#[context("prove_where_clause_well_formed({where_clause:?})")]
26+
// FIXME(oli-obk): figure out why is this a function and not a `judgment_fn`.
2627
fn prove_where_clause_well_formed(
2728
&self,
2829
in_env: &Env,
@@ -46,6 +47,13 @@ impl super::Check<'_> {
4647
self.prove_where_clause_well_formed(&e, assumptions, &wc)
4748
}
4849
WhereClauseData::TypeOfConst(ct, ty) => {
50+
match ct.data() {
51+
ConstData::Value(_, t) => {
52+
self.prove_goal(in_env, &assumptions, Relation::eq(ty, t))?
53+
}
54+
ConstData::Variable(_) => {}
55+
}
56+
// FIXME(oli-obk): prove that there is no `TypeOfConst` bound for a different type.
4957
self.prove_parameter_well_formed(in_env, &assumptions, ct.clone())?;
5058
self.prove_parameter_well_formed(in_env, assumptions, ty.clone())
5159
}

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use formality_types::{
2-
grammar::{Parameter, RigidName, RigidTy, UniversalVar, Wcs},
2+
grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs},
33
judgment_fn,
44
};
55

@@ -38,5 +38,11 @@ judgment_fn! {
3838
--- ("integers and booleans")
3939
(prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
4040
)
41+
42+
(
43+
(prove_wf(&decls, &env, &assumptions, ty) => c)
44+
--- ("rigid constants")
45+
(prove_wf(decls, env, assumptions, ConstData::Value(_, ty)) => c)
46+
)
4147
}
4248
}

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

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
mod valtree;
22

3-
use crate::cast::{Upcast, UpcastFrom};
3+
use crate::cast::{DowncastTo, Upcast, UpcastFrom};
44

55
use super::{Parameter, Ty, Variable};
66
use formality_macros::{term, Visit};
@@ -53,6 +53,28 @@ impl UpcastFrom<Self> for ConstData {
5353
}
5454
}
5555

56+
impl DowncastTo<ConstData> for Const {
57+
fn downcast_to(&self) -> Option<ConstData> {
58+
Some(self.data().clone())
59+
}
60+
}
61+
62+
impl DowncastTo<Const> for Parameter {
63+
fn downcast_to(&self) -> Option<Const> {
64+
match self {
65+
Parameter::Ty(_) | Parameter::Lt(_) => None,
66+
Parameter::Const(c) => Some(c.clone()),
67+
}
68+
}
69+
}
70+
71+
impl DowncastTo<ConstData> for Parameter {
72+
fn downcast_to(&self) -> Option<ConstData> {
73+
let c: Const = self.downcast_to()?;
74+
c.downcast_to()
75+
}
76+
}
77+
5678
#[term]
5779
pub enum Bool {
5880
#[grammar(true)]

tests/consts.rs

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -79,3 +79,57 @@ fn test_generic_mismatch() {
7979
]",
8080
));
8181
}
82+
83+
#[test]
84+
fn test_rigid_const_bound() {
85+
expect_test::expect![[r#"
86+
Ok(
87+
(),
88+
)
89+
"#]]
90+
.assert_debug_eq(&test_program_ok(
91+
"[
92+
crate Foo {
93+
trait Foo<> where [type_of_const true is bool] {}
94+
}
95+
]",
96+
));
97+
}
98+
99+
#[test]
100+
fn test_nonsense_rigid_const_bound() {
101+
expect_test::expect![[r#"
102+
Err(
103+
Error {
104+
context: "check_trait(Foo)",
105+
source: Error {
106+
context: "prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))",
107+
source: "failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}",
108+
},
109+
},
110+
)
111+
"#]]
112+
.assert_debug_eq(&test_program_ok(
113+
"[
114+
crate Foo {
115+
trait Foo<> where [type_of_const true is u32] {}
116+
}
117+
]",
118+
));
119+
}
120+
121+
#[test]
122+
fn test_multiple_type_of_const() {
123+
expect_test::expect![[r#"
124+
Ok(
125+
(),
126+
)
127+
"#]]
128+
.assert_debug_eq(&test_program_ok(
129+
"[
130+
crate Foo {
131+
trait Foo<const C> where [type_of_const C is bool, type_of_const C is u32] {}
132+
}
133+
]",
134+
));
135+
}

0 commit comments

Comments
 (0)