From 3314fe9b0e69abd689d97ededad75e4e15d7e9f4 Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 26 May 2022 14:42:24 +0200 Subject: [PATCH 1/4] add section on user types --- src/borrow_check/type_check.md | 41 ++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/src/borrow_check/type_check.md b/src/borrow_check/type_check.md index 1485f2ae8..c123ae33d 100644 --- a/src/borrow_check/type_check.md +++ b/src/borrow_check/type_check.md @@ -8,3 +8,44 @@ this type-check, we also uncover the region constraints that apply to the program. TODO -- elaborate further? Maybe? :) + +## User types + +At the start of MIR type-check, we replace all regions in the body with new unconstrained regions. +This would cause us to accept the following program however: +```rust +fn foo<'a>(x: &'a u32) { + let y: &'static u32 = x; +} +``` +By erasing the lifetimes in the type of `y` we no longer know that it is supposed to be `'static`, +ignoring the intentions of the user. + +To deal with this we remember all places where the user explicitly mentioned a type during hir typeck as +[`CanonicalUserTypeAnnotations`][annot]. + +There are two different annotations we care about: +- explicit type ascriptions, e.g. `let y: &'static u32` results in `UserType::Ty(&'static u32)`. +- explicit generic arguments, e.g. `x.foo<&'a u32, Vec>` results in `UserType::TypeOf(foo_def_id, [&'a u32, Vec])`. + +As we do not want the region inference from the hir typeck to influence MIR typeck, we store the user type right after lowering it from the hir. This means that it may still contain inference variables. This is the reason why we are dealing with **canonical** user type annotations. We replace all inference variables with existential bound variables instead. Something like `let x: Vec<_>` would therefore result in `exists UserType::Ty(Vec)`. + +A pattern like `let Foo(x): Foo<&'a u32>` has a user type `Foo<&'a u32>` but the actual type of `x` should only be `&'a u32`. For this, we use a [`UserTypeProjection`][proj]. + +In the MIR, we deal with user types in two slightly different ways. + +Given a MIR local corresponding to a variable in a pattern which has an explicit type annotation, we require the type of that local to be equal to the type of the [`UserTypeProjection`][proj]. This is directly stored in the [`LocalDecl`][decl]. + +We also constrain the type of scrutinee expressions, e.g. the type of `x` in `let _: &'a u32 = x;`. Here `T_x` only has to be a subtype of the user type, so we instead us [`StatementKind::AscribeUserType`][stmt] for that. + +Note that we do not directly user the user type as the MIR typechecker doesn't really deal with type and const inference variables. We instead store the final [`inferred_type`][inf] by the HIR typechecker. During MIR typeck, we then replace its regions with new nll inference vars and relate it with the actual `UserType` to get the correct region constraints again. + +After borrowch, all user type annotations get discarded, as they aren't needed anymore. + + + +[annot]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html +[proj]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.UserTypeProjection.html +[decl]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.LocalDecl.html +[stmt]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.StatementKind.html#variant.AscribeUserType +[inf]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html#structfield.inferred_ty \ No newline at end of file From 6f4dc860d95261d44252fffead90600e2609841b Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 26 May 2022 14:52:39 +0200 Subject: [PATCH 2/4] line length --- src/borrow_check/type_check.md | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/src/borrow_check/type_check.md b/src/borrow_check/type_check.md index c123ae33d..58b590139 100644 --- a/src/borrow_check/type_check.md +++ b/src/borrow_check/type_check.md @@ -21,24 +21,39 @@ fn foo<'a>(x: &'a u32) { By erasing the lifetimes in the type of `y` we no longer know that it is supposed to be `'static`, ignoring the intentions of the user. -To deal with this we remember all places where the user explicitly mentioned a type during hir typeck as -[`CanonicalUserTypeAnnotations`][annot]. +To deal with this we remember all places where the user explicitly mentioned a type during +hir typeck as [`CanonicalUserTypeAnnotations`][annot]. There are two different annotations we care about: - explicit type ascriptions, e.g. `let y: &'static u32` results in `UserType::Ty(&'static u32)`. -- explicit generic arguments, e.g. `x.foo<&'a u32, Vec>` results in `UserType::TypeOf(foo_def_id, [&'a u32, Vec])`. +- explicit generic arguments, e.g. `x.foo<&'a u32, Vec>` +results in `UserType::TypeOf(foo_def_id, [&'a u32, Vec])`. -As we do not want the region inference from the hir typeck to influence MIR typeck, we store the user type right after lowering it from the hir. This means that it may still contain inference variables. This is the reason why we are dealing with **canonical** user type annotations. We replace all inference variables with existential bound variables instead. Something like `let x: Vec<_>` would therefore result in `exists UserType::Ty(Vec)`. +As we do not want the region inference from the hir typeck to influence MIR typeck, +we store the user type right after lowering it from the hir. +This means that it may still contain inference variables, +which is why we are using **canonical** user type annotations. +We replace all inference variables with existential bound variables instead. +Something like `let x: Vec<_>` would therefore result in `exists UserType::Ty(Vec)`. -A pattern like `let Foo(x): Foo<&'a u32>` has a user type `Foo<&'a u32>` but the actual type of `x` should only be `&'a u32`. For this, we use a [`UserTypeProjection`][proj]. +A pattern like `let Foo(x): Foo<&'a u32>` has a user type `Foo<&'a u32>` but +the actual type of `x` should only be `&'a u32`. For this, we use a [`UserTypeProjection`][proj]. In the MIR, we deal with user types in two slightly different ways. -Given a MIR local corresponding to a variable in a pattern which has an explicit type annotation, we require the type of that local to be equal to the type of the [`UserTypeProjection`][proj]. This is directly stored in the [`LocalDecl`][decl]. +Given a MIR local corresponding to a variable in a pattern which has an explicit type annotation, +we require the type of that local to be equal to the type of the [`UserTypeProjection`][proj]. +This is directly stored in the [`LocalDecl`][decl]. -We also constrain the type of scrutinee expressions, e.g. the type of `x` in `let _: &'a u32 = x;`. Here `T_x` only has to be a subtype of the user type, so we instead us [`StatementKind::AscribeUserType`][stmt] for that. +We also constrain the type of scrutinee expressions, e.g. the type of `x` in `let _: &'a u32 = x;`. +Here `T_x` only has to be a subtype of the user type, so we instead use +[`StatementKind::AscribeUserType`][stmt] for that. -Note that we do not directly user the user type as the MIR typechecker doesn't really deal with type and const inference variables. We instead store the final [`inferred_type`][inf] by the HIR typechecker. During MIR typeck, we then replace its regions with new nll inference vars and relate it with the actual `UserType` to get the correct region constraints again. +Note that we do not directly use the user type as the MIR typechecker +doesn't really deal with type and const inference variables. We instead store the final +[`inferred_type`][inf] by the HIR typechecker. During MIR typeck, we then replace its regions +with new nll inference vars and relate it with the actual `UserType` to get the correct region +constraints again. After borrowch, all user type annotations get discarded, as they aren't needed anymore. From 550b941102d8757727602fef51490dc6abd03352 Mon Sep 17 00:00:00 2001 From: lcnr Date: Fri, 27 May 2022 08:34:50 +0200 Subject: [PATCH 3/4] review --- src/borrow_check/type_check.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/borrow_check/type_check.md b/src/borrow_check/type_check.md index 58b590139..5e9be39d2 100644 --- a/src/borrow_check/type_check.md +++ b/src/borrow_check/type_check.md @@ -12,7 +12,7 @@ TODO -- elaborate further? Maybe? :) ## User types At the start of MIR type-check, we replace all regions in the body with new unconstrained regions. -This would cause us to accept the following program however: +However, this would cause us to accept the following program: ```rust fn foo<'a>(x: &'a u32) { let y: &'static u32 = x; @@ -22,15 +22,15 @@ By erasing the lifetimes in the type of `y` we no longer know that it is suppose ignoring the intentions of the user. To deal with this we remember all places where the user explicitly mentioned a type during -hir typeck as [`CanonicalUserTypeAnnotations`][annot]. +HIR type-check as [`CanonicalUserTypeAnnotations`][annot]. There are two different annotations we care about: - explicit type ascriptions, e.g. `let y: &'static u32` results in `UserType::Ty(&'static u32)`. - explicit generic arguments, e.g. `x.foo<&'a u32, Vec>` results in `UserType::TypeOf(foo_def_id, [&'a u32, Vec])`. -As we do not want the region inference from the hir typeck to influence MIR typeck, -we store the user type right after lowering it from the hir. +As we do not want the region inference from the HIR type-check to influence MIR typeck, +we store the user type right after lowering it from the HIR. This means that it may still contain inference variables, which is why we are using **canonical** user type annotations. We replace all inference variables with existential bound variables instead. @@ -51,11 +51,11 @@ Here `T_x` only has to be a subtype of the user type, so we instead use Note that we do not directly use the user type as the MIR typechecker doesn't really deal with type and const inference variables. We instead store the final -[`inferred_type`][inf] by the HIR typechecker. During MIR typeck, we then replace its regions +[`inferred_type`][inf] from the HIR type-checker. During MIR typeck, we then replace its regions with new nll inference vars and relate it with the actual `UserType` to get the correct region constraints again. -After borrowch, all user type annotations get discarded, as they aren't needed anymore. +After the MIR type-check, all user type annotations get discarded, as they aren't needed anymore. From 53410ac2b6575591c4e5da9da76c3c2995ea012a Mon Sep 17 00:00:00 2001 From: Yuki Okushi Date: Sun, 5 Jun 2022 14:37:49 +0900 Subject: [PATCH 4/4] Update src/borrow_check/type_check.md --- src/borrow_check/type_check.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/borrow_check/type_check.md b/src/borrow_check/type_check.md index 5e9be39d2..69456d870 100644 --- a/src/borrow_check/type_check.md +++ b/src/borrow_check/type_check.md @@ -57,8 +57,6 @@ constraints again. After the MIR type-check, all user type annotations get discarded, as they aren't needed anymore. - - [annot]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.CanonicalUserTypeAnnotation.html [proj]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.UserTypeProjection.html [decl]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/struct.LocalDecl.html