@@ -39,10 +39,10 @@ describes why each variant exists.
39
39
40
40
### Application types
41
41
42
- The ` Apply ` variant contains an ` ApplicationTy ` . These are kind of the
43
- "normal Rust types", like ` Vec<u32> ` or ` f32 ` . They consist of a "type
44
- name" (in our examples, ` Vec ` and ` f32 ` respecively) and zero or more
45
- generic arguments (respectively, ` [u32] ` and ` [] ` ) .
42
+ Most of "normal rust types" like ` Vec<u32> ` or ` (f32, Vec<isize>) ` are represented with
43
+ ` TyKind ` variants containing some type-specific info ("type name") and a substitution
44
+ that is "applied" to that type. In this case, type names are ` Vec ` and "tuple of arity 2",
45
+ and substitutions are ` [u32] ` and ` [f32, Vec<isize>] ` .
46
46
47
47
They are equal to other types (modulo aliases, see below) iff they
48
48
have the same "type name" and the generic arguments are
@@ -61,17 +61,13 @@ placeholder. Similarly, in that same function, the associated type
61
61
Like application types, placeholder * types* are only known to be
62
62
equal.
63
63
64
- However, we choose not to represent placeholder types as type names
65
- because they need to be created during type unification and other
66
- operations, and hence that would require treating ` TypeName ` less opaquely.
67
-
68
- Moreover, when proving negative goals, e.g., `not { Implemented(T:
64
+ When proving negative goals, e.g., `not { Implemented(T:
69
65
Trait) }`, placeholders are treated quite differently from application
70
66
types, since they do not (in fact) represent a known type. When
71
- solving negative goals, placeholderes are replaced with inference
67
+ solving negative goals, placeholders are replaced with inference
72
68
variables -- the idea is that this goal is only true if there is * no
73
69
type* ` T ` that implements ` Trait ` . Therefore, if we can find no
74
- answeres for ` exists<T> { Implemented(T: Trait) } ` , then we know that
70
+ answers for ` exists<T> { Implemented(T: Trait) } ` , then we know that
75
71
the negation is true. (Note that this means that e.g. `forall<X > { X =
76
72
i32 }` is false but so is ` forall<X > { not { X = i32 } }`.)
77
73
@@ -110,16 +106,16 @@ that is outside the scope of the chalk-ir crate.
110
106
111
107
### Function pointer types
112
108
113
- The ` Fn ` variant wraps a ` FnTy ` struct and represents a ` fn() ` type
109
+ The ` Function ` variant wraps a ` FnPointer ` struct and represents a ` fn() ` type
114
110
(in other words, a function pointer). In some ways, fn types are like
115
111
application types, but with one crucial difference: they also contain
116
112
a ` forall ` binder that for lifetimes whose value is determined when
117
113
the function is called. Consider e.g. a type like ` fn(&u32) ` or --
118
114
more explicitly -- ` for<'a> fn(&'a u32) ` .
119
115
120
- Two ` Fn ` types ` A, B ` are equal ` A = B ` if ` A <: B ` and ` B <: A `
116
+ Two ` Function ` types ` A, B ` are equal ` A = B ` if ` A <: B ` and ` B <: A `
121
117
122
- Two ` Fn ` types ` A, B ` are subtypes ` A <: B ` if
118
+ Two ` Function ` types ` A, B ` are subtypes ` A <: B ` if
123
119
124
120
* After instantiating the lifetime parameters on ` B ` universally...
125
121
* You can instantiate the lifetime parameters on ` A ` existentially...
@@ -143,7 +139,7 @@ them in the [aliases chapter](./rust_types/alias.md).
143
139
144
140
### Bound variables
145
141
146
- The ` BoundVariable ` variant represents some variable that is bound in
142
+ The ` BoundVar ` variant represents some variable that is bound in
147
143
an outer term. For example, given a term like `forall<X > {
148
144
Implemented(X: Trait) }` , the ` X` is bound. Bound variables in chalk
149
145
(like rustc) use de bruijin indices (See below).
@@ -166,44 +162,41 @@ other type without any effect, and so forth.
166
162
167
163
## Mapping to rustc types
168
164
169
- The rustc [ ` TyKind ` ] enum has a lot more variants than chalk. This
165
+ The rustc [ ` TyKind ` ] enum is almost equivalent to chalk's . This
170
166
section describes how the rustc types can be mapped to chalk
171
167
types. The intention is that, at least when transitioning, rustc would
172
168
implement the ` Interner ` trait and would map from the [ ` TyKind ` ]
173
169
enum to chalk's ` TyKind ` on the fly, when ` data() ` is invoked.
174
170
175
171
[ `TyKind` ] : https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/enum.TyKind.html
176
172
177
- This section describes how each of rustc's variants can be mapped to
178
- Chalk variants.
179
-
180
173
| rustc type | chalk variant (and some notes) |
181
174
| ------------- | ------------------ |
182
- | ` Bool ` | ` Apply ` |
183
- | ` Char ` | ` Apply ` |
184
- | ` Int(_) ` | ` Apply ` |
185
- | ` Uint(_) ` | ` Apply ` |
186
- | ` Float(_) ` | ` Apply ` |
187
- | ` Adt(_, _) ` | ` Apply ` |
188
- | ` Foreign(_) ` | ` Apply ` |
189
- | ` Str ` | ` Apply ` |
190
- | ` Array(_, _) ` | ` Apply ` |
191
- | ` Slice(_) ` | ` Apply ` |
192
- | ` RawPtr(_) ` | ` Apply ` |
193
- | ` Ref(_, _, _) ` | ` Apply ` |
194
- | ` FnDef(_, _) ` | ` Apply ` |
195
- | ` FnPtr(_, _) ` | ` Fn ` |
196
- | ` Dynamic(_, _) ` | ` Dyn ` |
197
- | ` Closure(_, _) ` | ` Apply ` |
198
- | ` Generator(_, _) ` | ` Apply ` |
199
- | ` GeneratorWitness(_) ` | ` GeneratorWitness ` |
200
- | ` Never ` | ` Apply ` |
201
- | ` Tuple(_) ` | ` Apply ` |
202
- | ` Projection(_) ` | ` Alias ` |
203
- | ` UnnormalizedProjection(_) ` | (see below) |
204
- | ` Opaque(_, _) ` | ` Alias ` |
205
- | ` Param(_) ` | XXX Placeholder? |
206
- | ` Bound(_, _) ` | ` BoundVariable ` |
207
- | ` Placeholder(_) ` | ` Placeholder ` |
208
- | ` Infer(_) ` | ` InferenceVar ` |
175
+ | ` Bool ` | ` Scalar ` |
176
+ | ` Char ` | ` Scalar ` |
177
+ | ` Int ` | ` Scalar ` |
178
+ | ` Uint ` | ` Scalar ` |
179
+ | ` Float ` | ` Scalar ` |
180
+ | ` Adt ` | ` Adt ` |
181
+ | ` Foreign ` | ` Foreign ` |
182
+ | ` Str ` | ` Str ` |
183
+ | ` Array ` | ` Array ` |
184
+ | ` Slice ` | ` Slice ` |
185
+ | ` RawPtr ` | ` Raw ` |
186
+ | ` Ref ` | ` Ref ` |
187
+ | ` FnDef ` | ` FnDef ` |
188
+ | ` FnPtr ` | ` Function ` |
189
+ | ` Dynamic ` | ` Dyn ` |
190
+ | ` Closure ` | ` Closure ` |
191
+ | ` Generator ` | ` Generator ` |
192
+ | ` GeneratorWitness ` | ` GeneratorWitness ` |
193
+ | ` Never ` | ` Never ` |
194
+ | ` Tuple ` | ` Tuple ` |
195
+ | ` Projection ` | ` Alias ` |
196
+ | ` UnnormalizedProjection ` | (see below) |
197
+ | ` Opaque ` | ` Alias ` |
198
+ | ` Param ` | XXX Placeholder? |
199
+ | ` Bound ` | ` BoundVar ` |
200
+ | ` Placeholder ` | ` Placeholder ` |
201
+ | ` Infer ` | ` InferenceVar ` |
209
202
| ` Error ` | ` Error ` |
0 commit comments