Skip to content

Commit 005c483

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #293 from detrumi/quantifiedty-to-quantifiedapply
Change QuantifiedTy to QuantifiedApply
2 parents 4005b5f + 225665f commit 005c483

File tree

22 files changed

+93
-130
lines changed

22 files changed

+93
-130
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1037,12 +1037,11 @@ impl LowerTy for Ty {
10371037
.map(|id| chalk_ir::ParameterKind::Lifetime(id.str)),
10381038
)?;
10391039

1040-
let ty = ty.lower(&quantified_env)?;
1041-
let quantified_ty = chalk_ir::QuantifiedTy {
1040+
let function = chalk_ir::Fn {
10421041
num_binders: lifetime_names.len(),
1043-
ty,
1042+
parameters: vec![ty.lower(&quantified_env)?.cast()],
10441043
};
1045-
Ok(chalk_ir::TyData::ForAll(quantified_ty).intern())
1044+
Ok(chalk_ir::TyData::Function(function).intern())
10461045
}
10471046
}
10481047
}

‎chalk-ir/src/debug.rs

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ impl<TF: TypeFamily> Debug for TyData<TF> {
6363
TyData::Apply(apply) => write!(fmt, "{:?}", apply),
6464
TyData::Projection(proj) => write!(fmt, "{:?}", proj),
6565
TyData::Placeholder(index) => write!(fmt, "{:?}", index),
66-
TyData::ForAll(quantified_ty) => write!(fmt, "{:?}", quantified_ty),
66+
TyData::Function(function) => write!(fmt, "{:?}", function),
6767
}
6868
}
6969
}
@@ -81,11 +81,14 @@ impl Debug for InferenceVar {
8181
}
8282
}
8383

84-
impl<TF: TypeFamily> Debug for QuantifiedTy<TF> {
84+
impl<TF: TypeFamily> Debug for Fn<TF> {
8585
fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
8686
// FIXME -- we should introduce some names or something here
87-
let QuantifiedTy { num_binders, ty } = self;
88-
write!(fmt, "for<{}> {:?}", num_binders, ty)
87+
let Fn {
88+
num_binders,
89+
parameters,
90+
} = self;
91+
write!(fmt, "for<{}> {:?}", num_binders, parameters)
8992
}
9093
}
9194

‎chalk-ir/src/fold.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -324,9 +324,7 @@ where
324324
TyData::Projection(proj) => {
325325
Ok(TyData::Projection(proj.fold_with(folder, binders)?).intern())
326326
}
327-
TyData::ForAll(quantified_ty) => {
328-
Ok(TyData::ForAll(quantified_ty.fold_with(folder, binders)?).intern())
329-
}
327+
TyData::Function(fun) => Ok(TyData::Function(fun.fold_with(folder, binders)?).intern()),
330328
}
331329
}
332330

@@ -345,7 +343,7 @@ impl<TF: TypeFamily, TTF: TargetTypeFamily<TF>> Fold<TF, TTF> for Ty<TF> {
345343
}
346344
}
347345

348-
pub fn super_fold_lifetime<TF: TypeFamily, TTF: TargetTypeFamily<TF>>(
346+
pub fn super_fold_lifetime<TF: TypeFamily, TTF: TypeFamily>(
349347
folder: &mut dyn Folder<TF, TTF>,
350348
lifetime: &Lifetime<TF>,
351349
binders: usize,

‎chalk-ir/src/fold/binder_impls.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -6,20 +6,20 @@
66
use crate::family::TargetTypeFamily;
77
use crate::*;
88

9-
impl<TF: TypeFamily, TTF: TargetTypeFamily<TF>> Fold<TF, TTF> for QuantifiedTy<TF> {
10-
type Result = QuantifiedTy<TTF>;
9+
impl<TF: TypeFamily, TTF: TargetTypeFamily<TF>> Fold<TF, TTF> for Fn<TF> {
10+
type Result = Fn<TTF>;
1111
fn fold_with(
1212
&self,
1313
folder: &mut dyn Folder<TF, TTF>,
1414
binders: usize,
1515
) -> Fallible<Self::Result> {
16-
let QuantifiedTy {
16+
let Fn {
1717
num_binders,
18-
ref ty,
18+
ref parameters,
1919
} = *self;
20-
Ok(QuantifiedTy {
20+
Ok(Fn {
2121
num_binders,
22-
ty: ty.fold_with(folder, binders + num_binders)?,
22+
parameters: parameters.fold_with(folder, binders + num_binders)?,
2323
})
2424
}
2525
}

‎chalk-ir/src/fold/subst.rs

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,6 @@ impl<'s, TF: TypeFamily> Subst<'s, TF> {
1414
}
1515
}
1616

17-
impl<TF: TypeFamily> QuantifiedTy<TF> {
18-
pub fn substitute(&self, parameters: &[Parameter<TF>]) -> Ty<TF> {
19-
assert_eq!(self.num_binders, parameters.len());
20-
Subst::apply(parameters, &self.ty)
21-
}
22-
}
23-
2417
impl<'b, TF: TypeFamily> DefaultTypeFolder for Subst<'b, TF> {}
2518

2619
impl<'b, TF: TypeFamily> FreeVarFolder<TF> for Subst<'b, TF> {

‎chalk-ir/src/lib.rs

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -260,14 +260,11 @@ pub enum TyData<TF: TypeFamily> {
260260
/// trait and all its parameters are fully known.
261261
Projection(ProjectionTy<TF>),
262262

263-
/// A "higher-ranked" type. In the Rust surface syntax, this can
264-
/// only be a function type (e.g., `for<'a> fn(&'a u32)`) or a dyn
265-
/// type (e.g., `dyn for<'a> SomeTrait<&'a u32>`). However, in
266-
/// Chalk's representation, we separate out the `for<'a>` part
267-
/// from the underlying type, so technically we can represent
268-
/// things like `for<'a> SomeStruct<'a>`, although that has no
269-
/// meaning in Rust.
270-
ForAll(QuantifiedTy<TF>),
263+
/// A function type such as `for<'a> fn(&'a u32)`.
264+
/// Note that "higher-ranked" types (starting with `for<>`) are either
265+
/// function types or dyn types, and do not appear otherwise in Rust
266+
/// surface syntax.
267+
Function(Fn<TF>),
271268

272269
/// References the binding at the given depth. The index is a [de
273270
/// Bruijn index], so it counts back through the in-scope binders,
@@ -345,9 +342,9 @@ impl InferenceVar {
345342
/// for<'a...'z> X -- all binders are instantiated at once,
346343
/// and we use deBruijn indices within `self.ty`
347344
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasTypeFamily)]
348-
pub struct QuantifiedTy<TF: TypeFamily> {
345+
pub struct Fn<TF: TypeFamily> {
349346
pub num_binders: usize,
350-
pub ty: Ty<TF>,
347+
pub parameters: Vec<Parameter<TF>>,
351348
}
352349

353350
#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasTypeFamily)]

‎chalk-ir/src/macros.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ macro_rules! ty {
99
}).intern()
1010
};
1111

12-
(for_all $n:tt $t:tt) => {
13-
$crate::TyData::ForAll(QuantifiedTy {
12+
(function $n:tt $($arg:tt)*) => {
13+
$crate::TyData::Function(Fn {
1414
num_binders: $n,
15-
ty: ty!($t),
15+
parameters: vec![$(arg!($arg)),*],
1616
}).intern()
1717
};
1818

‎chalk-parse/src/parser.lalrpop

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,7 @@ AssocTyValue: AssocTyValue = {
165165
};
166166

167167
pub Ty: Ty = {
168-
"for" "<" <l:Comma<LifetimeId>> ">" <t:Ty> => Ty::ForAll {
168+
"for" "<" <l:Comma<LifetimeId>> ">" "fn" "(" <t:Ty> ")" => Ty::ForAll {
169169
lifetime_names: l,
170170
ty: Box::new(t)
171171
},
@@ -174,6 +174,10 @@ pub Ty: Ty = {
174174

175175
TyWithoutFor: Ty = {
176176
<n:Id> => Ty::Id { name: n},
177+
"fn" "(" <t:Ty> ")" => Ty::ForAll {
178+
lifetime_names: vec![],
179+
ty: Box::new(t)
180+
},
177181
"dyn" <b:Plus<QuantifiedInlineBound>> => Ty::Dyn {
178182
bounds: b,
179183
},

‎chalk-solve/src/clauses.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -341,7 +341,11 @@ fn match_ty<TF: TypeFamily>(
341341
.db
342342
.associated_ty_data(projection_ty.associated_ty_id)
343343
.to_program_clauses(builder),
344-
TyData::ForAll(quantified_ty) => match_ty(builder, environment, &quantified_ty.ty),
344+
TyData::Function(quantified_ty) => quantified_ty
345+
.parameters
346+
.iter()
347+
.map(|p| p.assert_ty_ref())
348+
.for_each(|ty| match_ty(builder, environment, &ty)),
345349
TyData::BoundVar(_) => {}
346350
TyData::InferenceVar(_) => panic!("should have floundered"),
347351
TyData::Dyn(_) => {}

‎chalk-solve/src/clauses/env_elaborator.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,7 @@ impl<'me, TF: TypeFamily> EnvElaborator<'me, TF> {
6464
// bounds story around `dyn Trait` types.
6565
TyData::Dyn(_) => (),
6666

67-
TyData::ForAll(_) | TyData::BoundVar(_) | TyData::InferenceVar(_) => (),
67+
TyData::Function(_) | TyData::BoundVar(_) | TyData::InferenceVar(_) => (),
6868
}
6969
}
7070

‎chalk-solve/src/infer/instantiate.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -112,20 +112,20 @@ impl<'a, T> IntoBindersAndValue for &'a Binders<T> {
112112
}
113113
}
114114

115-
impl<'a, TF> IntoBindersAndValue for &'a QuantifiedTy<TF>
115+
impl<'a, TF> IntoBindersAndValue for &'a Fn<TF>
116116
where
117117
TF: TypeFamily,
118118
{
119119
type Binders = std::iter::Map<std::ops::Range<usize>, fn(usize) -> chalk_ir::ParameterKind<()>>;
120-
type Value = &'a Ty<TF>;
120+
type Value = &'a Vec<Parameter<TF>>;
121121

122122
fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
123123
fn make_lifetime(_: usize) -> ParameterKind<()> {
124124
ParameterKind::Lifetime(())
125125
}
126126

127127
let p: fn(usize) -> ParameterKind<()> = make_lifetime;
128-
((0..self.num_binders).map(p), &self.ty)
128+
((0..self.num_binders).map(p), &self.parameters)
129129
}
130130
}
131131

‎chalk-solve/src/infer/test.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ fn cycle_error() {
4646

4747
// exists(A -> A = for<'a> A)
4848
table
49-
.unify(&environment0, &a, &ty!(for_all 1 (infer 0)))
49+
.unify(&environment0, &a, &ty!(function 1 (infer 0)))
5050
.unwrap_err();
5151
}
5252

@@ -215,18 +215,18 @@ fn quantify_ty_under_binder() {
215215
.unify(&environment0, &v0.to_ty(), &v1.to_ty())
216216
.unwrap();
217217

218-
// Here: the `for_all` introduces 3 binders, so in the result,
218+
// Here: the `function` introduces 3 binders, so in the result,
219219
// `(bound 3)` references the first canonicalized inference
220220
// variable. -- note that `infer 0` and `infer 1` have been
221221
// unified above, as well.
222222
assert_eq!(
223223
table
224224
.canonicalize(
225-
&ty!(for_all 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2))))
225+
&ty!(function 3 (apply (item 0) (bound 1) (infer 0) (infer 1) (lifetime (infer 2))))
226226
)
227227
.quantified,
228228
Canonical {
229-
value: ty!(for_all 3 (apply (item 0) (bound 1) (bound 3) (bound 3) (lifetime (bound 4)))),
229+
value: ty!(function 3 (apply (item 0) (bound 1) (bound 3) (bound 3) (lifetime (bound 4)))),
230230
binders: vec![ParameterKind::Ty(U0), ParameterKind::Lifetime(U0)],
231231
}
232232
);

‎chalk-solve/src/infer/unify.rs

Lines changed: 15 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -77,19 +77,6 @@ impl<'t, TF: TypeFamily> Unifier<'t, TF> {
7777
})
7878
}
7979

80-
/// When we encounter a "sub-unification" problem that is in a distinct
81-
/// environment, we invoke this routine.
82-
fn sub_unify<T>(&mut self, ty1: T, ty2: T) -> Fallible<()>
83-
where
84-
T: Zip<TF> + Fold<TF>,
85-
{
86-
let sub_unifier = Unifier::new(self.table, &self.environment);
87-
let UnificationResult { goals, constraints } = sub_unifier.unify(&ty1, &ty2)?;
88-
self.goals.extend(goals);
89-
self.constraints.extend(constraints);
90-
Ok(())
91-
}
92-
9380
fn unify_ty_ty<'a>(&mut self, a: &'a Ty<TF>, b: &'a Ty<TF>) -> Fallible<()> {
9481
// ^^ ^^ ^^ FIXME rustc bug
9582
if let Some(n_a) = self.table.normalize_shallow(a) {
@@ -123,29 +110,27 @@ impl<'t, TF: TypeFamily> Unifier<'t, TF> {
123110
(&TyData::InferenceVar(var), &TyData::Apply(_))
124111
| (&TyData::InferenceVar(var), &TyData::Placeholder(_))
125112
| (&TyData::InferenceVar(var), &TyData::Dyn(_))
126-
| (&TyData::InferenceVar(var), &TyData::ForAll(_)) => self.unify_var_ty(var, b),
113+
| (&TyData::InferenceVar(var), &TyData::Function(_)) => self.unify_var_ty(var, b),
127114

128115
(&TyData::Apply(_), &TyData::InferenceVar(var))
129116
| (&TyData::Placeholder(_), &TyData::InferenceVar(var))
130117
| (&TyData::Dyn(_), &TyData::InferenceVar(var))
131-
| (&TyData::ForAll(_), &TyData::InferenceVar(var)) => self.unify_var_ty(var, a),
118+
| (&TyData::Function(_), &TyData::InferenceVar(var)) => self.unify_var_ty(var, a),
132119

133120
// Unifying `forall<X> { T }` with some other forall type `forall<X> { U }`
134-
(&TyData::ForAll(ref quantified_ty1), &TyData::ForAll(ref quantified_ty2)) => {
135-
self.unify_binders(quantified_ty1, quantified_ty2)
121+
(&TyData::Function(ref fn1), &TyData::Function(ref fn2)) => {
122+
self.unify_binders(fn1, fn2)
136123
}
137124

138-
// Unifying `forall<X> { T }` with some other type `U`
139-
(&TyData::ForAll(ref quantified_ty), &TyData::Apply(_))
140-
| (&TyData::ForAll(ref quantified_ty), &TyData::Placeholder(_))
141-
| (&TyData::ForAll(ref quantified_ty), &TyData::Dyn(_)) => {
142-
self.unify_forall_other(quantified_ty, b)
143-
}
144-
145-
(&TyData::Apply(_), &TyData::ForAll(ref quantified_ty))
146-
| (&TyData::Placeholder(_), &TyData::ForAll(ref quantified_ty))
147-
| (&TyData::Dyn(_), &TyData::ForAll(ref quantified_ty)) => {
148-
self.unify_forall_other(quantified_ty, a)
125+
// This would correspond to unifying a `fn` type with a non-fn
126+
// type in Rust; error.
127+
(&TyData::Function(_), &TyData::Apply(_))
128+
| (&TyData::Function(_), &TyData::Dyn(_))
129+
| (&TyData::Function(_), &TyData::Placeholder(_))
130+
| (&TyData::Apply(_), &TyData::Function(_))
131+
| (&TyData::Placeholder(_), &TyData::Function(_))
132+
| (&TyData::Dyn(_), &TyData::Function(_)) => {
133+
return Err(NoSolution);
149134
}
150135

151136
(&TyData::Placeholder(ref p1), &TyData::Placeholder(ref p2)) => {
@@ -177,14 +162,14 @@ impl<'t, TF: TypeFamily> Unifier<'t, TF> {
177162
// Trait>::Item` with some other type `U`.
178163
(&TyData::Apply(_), &TyData::Projection(ref proj))
179164
| (&TyData::Placeholder(_), &TyData::Projection(ref proj))
180-
| (&TyData::ForAll(_), &TyData::Projection(ref proj))
165+
| (&TyData::Function(_), &TyData::Projection(ref proj))
181166
| (&TyData::InferenceVar(_), &TyData::Projection(ref proj))
182167
| (&TyData::Dyn(_), &TyData::Projection(ref proj)) => self.unify_projection_ty(proj, a),
183168

184169
(&TyData::Projection(ref proj), &TyData::Projection(_))
185170
| (&TyData::Projection(ref proj), &TyData::Apply(_))
186171
| (&TyData::Projection(ref proj), &TyData::Placeholder(_))
187-
| (&TyData::Projection(ref proj), &TyData::ForAll(_))
172+
| (&TyData::Projection(ref proj), &TyData::Function(_))
188173
| (&TyData::Projection(ref proj), &TyData::InferenceVar(_))
189174
| (&TyData::Projection(ref proj), &TyData::Dyn(_)) => self.unify_projection_ty(proj, b),
190175

@@ -243,26 +228,6 @@ impl<'t, TF: TypeFamily> Unifier<'t, TF> {
243228
)))
244229
}
245230

246-
/// Unifying `forall<X> { T }` with some other type `U` --
247-
/// to do so, we create a fresh placeholder `P` for `X` and
248-
/// see if `[X/Px] T` can be unified with `U`. This should
249-
/// almost never be true, actually, unless `X` is unused.
250-
fn unify_forall_other(&mut self, ty1: &QuantifiedTy<TF>, ty2: &Ty<TF>) -> Fallible<()> {
251-
let ui = self.table.new_universe();
252-
let lifetimes1: Vec<_> = (0..ty1.num_binders)
253-
.map(|idx| {
254-
LifetimeData::Placeholder(PlaceholderIndex { ui, idx })
255-
.intern()
256-
.cast()
257-
})
258-
.collect();
259-
260-
let ty1 = ty1.substitute(&lifetimes1);
261-
let ty2 = ty2.clone();
262-
263-
self.sub_unify(ty1, ty2)
264-
}
265-
266231
/// Unify an inference variable `var` with some non-inference
267232
/// variable `ty`, just bind `var` to `ty`. But we must enforce two conditions:
268233
///

‎chalk-solve/src/solve/slg.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -527,7 +527,7 @@ impl MayInvalidate {
527527
}
528528

529529
// For everything else, be conservative here and just say we may invalidate.
530-
(TyData::ForAll(_), _)
530+
(TyData::Function(_), _)
531531
| (TyData::Dyn(_), _)
532532
| (TyData::Apply(_), _)
533533
| (TyData::Placeholder(_), _)

‎chalk-solve/src/solve/slg/aggregate.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,7 @@ impl<TF: TypeFamily> AntiUnifier<'_, TF> {
180180
// kinda hard. Don't try to be smart for now, just plop a
181181
// variable in there and be done with it.
182182
(TyData::BoundVar(_), TyData::BoundVar(_))
183-
| (TyData::ForAll(_), TyData::ForAll(_))
183+
| (TyData::Function(_), TyData::Function(_))
184184
| (TyData::Dyn(_), TyData::Dyn(_)) => self.new_variable(),
185185

186186
(TyData::Apply(apply1), TyData::Apply(apply2)) => {
@@ -199,7 +199,7 @@ impl<TF: TypeFamily> AntiUnifier<'_, TF> {
199199
(TyData::InferenceVar(_), _)
200200
| (TyData::BoundVar(_), _)
201201
| (TyData::Dyn(_), _)
202-
| (TyData::ForAll(_), _)
202+
| (TyData::Function(_), _)
203203
| (TyData::Apply(_), _)
204204
| (TyData::Projection(_), _)
205205
| (TyData::Placeholder(_), _) => self.new_variable(),

0 commit comments

Comments
 (0)