Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

integrate MIR type-checker with NLL inference #45825

Merged
merged 65 commits into from
Nov 16, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
65 commits
Select commit Hold shift + click to select a range
4afe423
fulfill: remove dead code
nikomatsakis Nov 1, 2017
64206b4
move region constraints into inference context
nikomatsakis Nov 1, 2017
0d78e40
convert EXTRA_REQUIREMENT_IN_IMPL into a hard error
nikomatsakis Nov 1, 2017
c925008
assert that we are consuming all of the region obligations
nikomatsakis Nov 1, 2017
d73be85
extract `regionck_outlives` into a separate helper function
nikomatsakis Nov 2, 2017
22cd041
move the `region_obligations` processing code into `InferCtxt`
nikomatsakis Nov 3, 2017
e0630e8
refactor how we extract outlives bounds from trait definitions
nikomatsakis Nov 3, 2017
3cc44a5
do not invoke `required_region_bounds` in `region_obligations`
nikomatsakis Nov 4, 2017
b587c1a
regionck: only add implied bounds from root fn to `free_region_map`
nikomatsakis Nov 4, 2017
0c81d01
extract out the implied bounds code from `regionck`
nikomatsakis Nov 4, 2017
56e5eb5
rename mod `region_obligations` to `outlives::obligations`
nikomatsakis Nov 4, 2017
15a2dfa
move the `OutlivesEnvironment` into `infer` so that `nll` can use it
nikomatsakis Nov 4, 2017
6d67296
thread location info through mir typeck (but do not use)
nikomatsakis Nov 4, 2017
9e8abd7
apply rustfmt to `type_check`
nikomatsakis Nov 4, 2017
efa09db
modify MIR type-checker to process obligations as they are incurred
nikomatsakis Nov 5, 2017
467f2ea
extract lexical region resolution into its own sub-module
nikomatsakis Nov 5, 2017
58c7760
move region resolution to be a sibling of `region_inference`
nikomatsakis Nov 15, 2017
ef5de07
fix rename to block_data in type_check.rs
nikomatsakis Nov 15, 2017
9d63330
region_inference: tighten up `pub`, stop re-exporting enum variants
nikomatsakis Nov 5, 2017
8e9e154
region_inference: extract taint into a sub-module
nikomatsakis Nov 5, 2017
b769785
move `RegionResolutionError` into `lexical_region_resolve`
nikomatsakis Nov 5, 2017
ec48b01
extract storage of region values from `RegionVarBindings`
nikomatsakis Nov 5, 2017
daceedf
region_inference: rustfmt
nikomatsakis Nov 5, 2017
63d658d
extract the `tcx` out from `RegionVarBindings`
nikomatsakis Nov 5, 2017
cff191d
move refcells out from `RegionVarBindings` and up into `InferCtxt`
nikomatsakis Nov 5, 2017
23abd85
rename `region_inference` module to `region_constraints`
nikomatsakis Nov 5, 2017
48d8f72
infer: rename `region_vars` field to `region_constraints`
nikomatsakis Nov 5, 2017
326ec52
rename RegionVarBindings to RegionConstraintCollector
nikomatsakis Nov 5, 2017
adf1519
make the `region_constraints` field an `Option`
nikomatsakis Nov 5, 2017
f6037f2
separate the `Collector` from the `Data` it is collecting
nikomatsakis Nov 5, 2017
bea6b94
fix error messages relating to removing lint for E0276
nikomatsakis Nov 5, 2017
524e23a
make `RegionVid` implement `Idx` and use `IndexVec`
nikomatsakis Nov 5, 2017
a8daa37
region_constraints: only push givens into undo-log if in a snapshot
nikomatsakis Nov 5, 2017
1efcf1a
split the `var_origins` from the `RegionConstraintData`
nikomatsakis Nov 5, 2017
1430a60
add method `take_and_reset_region_constraints` to `InferCtxt`
nikomatsakis Nov 5, 2017
034018c
rustfmt `lexical_region_resolve`
nikomatsakis Nov 5, 2017
37945fe
MIR typeck: rustfmt
nikomatsakis Nov 7, 2017
ad93b69
MIR typeck: refactor to track region constraints
nikomatsakis Nov 5, 2017
89c1b60
replace `usize` with `RegionIndex` in indices map
nikomatsakis Nov 6, 2017
72675d8
replace `RegionIndex` with `RegionVid` (which now impls Idx)
nikomatsakis Nov 6, 2017
09b44bb
IndexVec: add `'_` to make clear where borrowing is happening
nikomatsakis Nov 6, 2017
a87d1bb
infer: give access to region variable origins
nikomatsakis Nov 6, 2017
109c9a7
infer: extract total number of region variables from infcx
nikomatsakis Nov 6, 2017
51ce1f9
formalize giving ownership of region vars to region inf. context
nikomatsakis Nov 6, 2017
ef392bc
simplify lifetime annotations for `MirBorrowckCtxt`
nikomatsakis Nov 7, 2017
8d3219e
erase regions in MIR borrowck when checking if type moves by default
nikomatsakis Nov 6, 2017
5592bb7
MIR-dump: print return type from local_decls for `_0`
nikomatsakis Nov 7, 2017
12534e9
renumber: handle ReturnTy better
nikomatsakis Nov 7, 2017
32f964c
renumber: debug logs, use `visit_region` rather than `visit_rvalue`
nikomatsakis Nov 7, 2017
d9e841e
region_infer: improved debug logging
nikomatsakis Nov 7, 2017
4b743da
integrate NLL with MIR type-checker
nikomatsakis Nov 6, 2017
b383ab7
update READMEs to describe the new situation
nikomatsakis Nov 7, 2017
013f88b
infer/outlives: add license
nikomatsakis Nov 7, 2017
267574c
convert TODO in traits into a FIXME
nikomatsakis Nov 7, 2017
9da54c1
add FIXME for converting RegionVid to use `newtype_index!`
nikomatsakis Nov 7, 2017
8cea053
fix mir-opt NLL tests -- variable `'_#0r` is now `'static`
nikomatsakis Nov 7, 2017
c7c2603
factor out `free_region_binding_scope` helper
nikomatsakis Nov 7, 2017
5a8c1eb
leak the affects of closures on the free-region-map, like we used to
nikomatsakis Nov 7, 2017
f722591
Nit: fix wording in README
nikomatsakis Nov 14, 2017
15739b8
Nit: rework region obligations to a snapshotted vector
nikomatsakis Nov 14, 2017
11c84c6
Nit: improve comment to explain why we wait until regionck
nikomatsakis Nov 14, 2017
a73d620
Nit: reset more state after `take_and_reset_data`
nikomatsakis Nov 14, 2017
a94d2a6
Nit: fix typo
nikomatsakis Nov 15, 2017
9e29662
obligations.rs: rustfmt
nikomatsakis Nov 16, 2017
8c109f5
infer/outlives/obligations.rs: wrap some long lines
nikomatsakis Nov 16, 2017
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
438 changes: 213 additions & 225 deletions src/librustc/infer/README.md

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion src/librustc/infer/equate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,8 @@ impl<'combine, 'infcx, 'gcx, 'tcx> TypeRelation<'infcx, 'gcx, 'tcx>
a,
b);
let origin = Subtype(self.fields.trace.clone());
self.fields.infcx.region_vars.make_eqregion(origin, a, b);
self.fields.infcx.borrow_region_constraints()
.make_eqregion(origin, a, b);
Ok(a)
}

Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/error_reporting/different_lifetimes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@
use hir;
use infer::InferCtxt;
use ty::{self, Region};
use infer::region_inference::RegionResolutionError::*;
use infer::region_inference::RegionResolutionError;
use infer::lexical_region_resolve::RegionResolutionError::*;
use infer::lexical_region_resolve::RegionResolutionError;
use hir::map as hir_map;
use middle::resolve_lifetime as rl;
use hir::intravisit::{self, Visitor, NestedVisitorMap};
Expand Down
76 changes: 37 additions & 39 deletions src/librustc/infer/error_reporting/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,8 +57,8 @@

use infer;
use super::{InferCtxt, TypeTrace, SubregionOrigin, RegionVariableOrigin, ValuePairs};
use super::region_inference::{RegionResolutionError, ConcreteFailure, SubSupConflict,
GenericBoundFailure, GenericKind};
use super::region_constraints::GenericKind;
use super::lexical_region_resolve::RegionResolutionError;

use std::fmt;
use hir;
Expand Down Expand Up @@ -177,13 +177,7 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {

ty::ReEarlyBound(_) |
ty::ReFree(_) => {
let scope = match *region {
ty::ReEarlyBound(ref br) => {
self.parent_def_id(br.def_id).unwrap()
}
ty::ReFree(ref fr) => fr.scope,
_ => bug!()
};
let scope = region.free_region_binding_scope(self);
let prefix = match *region {
ty::ReEarlyBound(ref br) => {
format!("the lifetime {} as defined on", br.name)
Expand Down Expand Up @@ -293,33 +287,37 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
debug!("report_region_errors: error = {:?}", error);

if !self.try_report_named_anon_conflict(&error) &&
!self.try_report_anon_anon_conflict(&error) {

match error.clone() {
// These errors could indicate all manner of different
// problems with many different solutions. Rather
// than generate a "one size fits all" error, what we
// attempt to do is go through a number of specific
// scenarios and try to find the best way to present
// the error. If all of these fails, we fall back to a rather
// general bit of code that displays the error information
ConcreteFailure(origin, sub, sup) => {
self.report_concrete_failure(region_scope_tree, origin, sub, sup).emit();
}

GenericBoundFailure(kind, param_ty, sub) => {
self.report_generic_bound_failure(region_scope_tree, kind, param_ty, sub);
}

SubSupConflict(var_origin, sub_origin, sub_r, sup_origin, sup_r) => {
!self.try_report_anon_anon_conflict(&error)
{
match error.clone() {
// These errors could indicate all manner of different
// problems with many different solutions. Rather
// than generate a "one size fits all" error, what we
// attempt to do is go through a number of specific
// scenarios and try to find the best way to present
// the error. If all of these fails, we fall back to a rather
// general bit of code that displays the error information
RegionResolutionError::ConcreteFailure(origin, sub, sup) => {
self.report_concrete_failure(region_scope_tree, origin, sub, sup).emit();
}

RegionResolutionError::GenericBoundFailure(kind, param_ty, sub) => {
self.report_generic_bound_failure(region_scope_tree, kind, param_ty, sub);
}

RegionResolutionError::SubSupConflict(var_origin,
sub_origin,
sub_r,
sup_origin,
sup_r) => {
self.report_sub_sup_conflict(region_scope_tree,
var_origin,
sub_origin,
sub_r,
sup_origin,
sup_r);
}
}
}
}
}
}
}
Expand Down Expand Up @@ -351,9 +349,9 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
// the only thing in the list.

let is_bound_failure = |e: &RegionResolutionError<'tcx>| match *e {
ConcreteFailure(..) => false,
SubSupConflict(..) => false,
GenericBoundFailure(..) => true,
RegionResolutionError::GenericBoundFailure(..) => true,
RegionResolutionError::ConcreteFailure(..) |
RegionResolutionError::SubSupConflict(..) => false,
};


Expand All @@ -365,9 +363,9 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {

// sort the errors by span, for better error message stability.
errors.sort_by_key(|u| match *u {
ConcreteFailure(ref sro, _, _) => sro.span(),
GenericBoundFailure(ref sro, _, _) => sro.span(),
SubSupConflict(ref rvo, _, _, _, _) => rvo.span(),
RegionResolutionError::ConcreteFailure(ref sro, _, _) => sro.span(),
RegionResolutionError::GenericBoundFailure(ref sro, _, _) => sro.span(),
RegionResolutionError::SubSupConflict(ref rvo, _, _, _, _) => rvo.span(),
});
errors
}
Expand Down Expand Up @@ -880,14 +878,13 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
};

if let SubregionOrigin::CompareImplMethodObligation {
span, item_name, impl_item_def_id, trait_item_def_id, lint_id
span, item_name, impl_item_def_id, trait_item_def_id,
} = origin {
self.report_extra_impl_obligation(span,
item_name,
impl_item_def_id,
trait_item_def_id,
&format!("`{}: {}`", bound_kind, sub),
lint_id)
&format!("`{}: {}`", bound_kind, sub))
.emit();
return;
}
Expand Down Expand Up @@ -1026,6 +1023,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
let var_name = self.tcx.hir.name(var_node_id);
format!(" for capture of `{}` by closure", var_name)
}
infer::NLL(..) => bug!("NLL variable found in lexical phase"),
};

struct_span_err!(self.tcx.sess, var_origin.span(), E0495,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok

Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/error_reporting/named_anon_conflict.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@
//! Error Reporting for Anonymous Region Lifetime Errors
//! where one region is named and the other is anonymous.
use infer::InferCtxt;
use infer::region_inference::RegionResolutionError::*;
use infer::region_inference::RegionResolutionError;
use infer::lexical_region_resolve::RegionResolutionError::*;
use infer::lexical_region_resolve::RegionResolutionError;
use ty;

impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
Expand Down
6 changes: 2 additions & 4 deletions src/librustc/infer/error_reporting/note.rs
Original file line number Diff line number Diff line change
Expand Up @@ -445,14 +445,12 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
infer::CompareImplMethodObligation { span,
item_name,
impl_item_def_id,
trait_item_def_id,
lint_id } => {
trait_item_def_id } => {
self.report_extra_impl_obligation(span,
item_name,
impl_item_def_id,
trait_item_def_id,
&format!("`{}: {}`", sup, sub),
lint_id)
&format!("`{}: {}`", sup, sub))
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/fudge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
self.type_variables.borrow_mut().types_created_since_snapshot(
&snapshot.type_snapshot);
let region_vars =
self.region_vars.vars_created_since_snapshot(
&snapshot.region_vars_snapshot);
self.borrow_region_constraints().vars_created_since_snapshot(
&snapshot.region_constraints_snapshot);

Ok((type_variables, region_vars, value))
}
Expand Down
2 changes: 1 addition & 1 deletion src/librustc/infer/glb.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ impl<'combine, 'infcx, 'gcx, 'tcx> TypeRelation<'infcx, 'gcx, 'tcx>
b);

let origin = Subtype(self.fields.trace.clone());
Ok(self.fields.infcx.region_vars.glb_regions(origin, a, b))
Ok(self.fields.infcx.borrow_region_constraints().glb_regions(self.tcx(), origin, a, b))
}

fn binders<T>(&mut self, a: &ty::Binder<T>, b: &ty::Binder<T>)
Expand Down
26 changes: 17 additions & 9 deletions src/librustc/infer/higher_ranked/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ use super::{CombinedSnapshot,
SubregionOrigin,
SkolemizationMap};
use super::combine::CombineFields;
use super::region_inference::{TaintDirections};
use super::region_constraints::{TaintDirections};

use ty::{self, TyCtxt, Binder, TypeFoldable};
use ty::error::TypeError;
Expand Down Expand Up @@ -176,9 +176,10 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
.filter(|&r| r != representative)
{
let origin = SubregionOrigin::Subtype(self.trace.clone());
self.infcx.region_vars.make_eqregion(origin,
*representative,
*region);
self.infcx.borrow_region_constraints()
.make_eqregion(origin,
*representative,
*region);
}
}

Expand Down Expand Up @@ -427,7 +428,7 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
fn fresh_bound_variable<'a, 'gcx, 'tcx>(infcx: &InferCtxt<'a, 'gcx, 'tcx>,
debruijn: ty::DebruijnIndex)
-> ty::Region<'tcx> {
infcx.region_vars.new_bound(debruijn)
infcx.borrow_region_constraints().new_bound(infcx.tcx, debruijn)
}
}
}
Expand Down Expand Up @@ -481,7 +482,11 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
r: ty::Region<'tcx>,
directions: TaintDirections)
-> FxHashSet<ty::Region<'tcx>> {
self.region_vars.tainted(&snapshot.region_vars_snapshot, r, directions)
self.borrow_region_constraints().tainted(
self.tcx,
&snapshot.region_constraints_snapshot,
r,
directions)
}

fn region_vars_confined_to_snapshot(&self,
Expand Down Expand Up @@ -539,7 +544,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
*/

let mut region_vars =
self.region_vars.vars_created_since_snapshot(&snapshot.region_vars_snapshot);
self.borrow_region_constraints().vars_created_since_snapshot(
&snapshot.region_constraints_snapshot);

let escaping_types =
self.type_variables.borrow_mut().types_escaping_snapshot(&snapshot.type_snapshot);
Expand Down Expand Up @@ -581,7 +587,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
where T : TypeFoldable<'tcx>
{
let (result, map) = self.tcx.replace_late_bound_regions(binder, |br| {
self.region_vars.push_skolemized(br, &snapshot.region_vars_snapshot)
self.borrow_region_constraints()
.push_skolemized(self.tcx, br, &snapshot.region_constraints_snapshot)
});

debug!("skolemize_bound_regions(binder={:?}, result={:?}, map={:?})",
Expand Down Expand Up @@ -766,7 +773,8 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
{
debug!("pop_skolemized({:?})", skol_map);
let skol_regions: FxHashSet<_> = skol_map.values().cloned().collect();
self.region_vars.pop_skolemized(&skol_regions, &snapshot.region_vars_snapshot);
self.borrow_region_constraints()
.pop_skolemized(self.tcx, &skol_regions, &snapshot.region_constraints_snapshot);
if !skol_map.is_empty() {
self.projection_cache.borrow_mut().rollback_skolemized(
&snapshot.projection_cache_snapshot);
Expand Down
Original file line number Diff line number Diff line change
@@ -1,10 +1,13 @@
Region inference
# Region inference

# Terminology
## Terminology

Note that we use the terms region and lifetime interchangeably.

# Introduction
## Introduction

See the [general inference README](../README.md) for an overview of
how lexical-region-solving fits into the bigger picture.

Region inference uses a somewhat more involved algorithm than type
inference. It is not the most efficient thing ever written though it
Expand All @@ -16,63 +19,6 @@ it's worth spending more time on a more involved analysis. Moreover,
regions are a simpler case than types: they don't have aggregate
structure, for example.

Unlike normal type inference, which is similar in spirit to H-M and thus
works progressively, the region type inference works by accumulating
constraints over the course of a function. Finally, at the end of
processing a function, we process and solve the constraints all at
once.

The constraints are always of one of three possible forms:

- `ConstrainVarSubVar(Ri, Rj)` states that region variable Ri must be
a subregion of Rj
- `ConstrainRegSubVar(R, Ri)` states that the concrete region R (which
must not be a variable) must be a subregion of the variable Ri
- `ConstrainVarSubReg(Ri, R)` states the variable Ri shoudl be less
than the concrete region R. This is kind of deprecated and ought to
be replaced with a verify (they essentially play the same role).

In addition to constraints, we also gather up a set of "verifys"
(what, you don't think Verify is a noun? Get used to it my
friend!). These represent relations that must hold but which don't
influence inference proper. These take the form of:

- `VerifyRegSubReg(Ri, Rj)` indicates that Ri <= Rj must hold,
where Rj is not an inference variable (and Ri may or may not contain
one). This doesn't influence inference because we will already have
inferred Ri to be as small as possible, so then we just test whether
that result was less than Rj or not.
- `VerifyGenericBound(R, Vb)` is a more complex expression which tests
that the region R must satisfy the bound `Vb`. The bounds themselves
may have structure like "must outlive one of the following regions"
or "must outlive ALL of the following regions. These bounds arise
from constraints like `T: 'a` -- if we know that `T: 'b` and `T: 'c`
(say, from where clauses), then we can conclude that `T: 'a` if `'b:
'a` *or* `'c: 'a`.

# Building up the constraints

Variables and constraints are created using the following methods:

- `new_region_var()` creates a new, unconstrained region variable;
- `make_subregion(Ri, Rj)` states that Ri is a subregion of Rj
- `lub_regions(Ri, Rj) -> Rk` returns a region Rk which is
the smallest region that is greater than both Ri and Rj
- `glb_regions(Ri, Rj) -> Rk` returns a region Rk which is
the greatest region that is smaller than both Ri and Rj

The actual region resolution algorithm is not entirely
obvious, though it is also not overly complex.

## Snapshotting

It is also permitted to try (and rollback) changes to the graph. This
is done by invoking `start_snapshot()`, which returns a value. Then
later you can call `rollback_to()` which undoes the work.
Alternatively, you can call `commit()` which ends all snapshots.
Snapshots can be recursive---so you can start a snapshot when another
is in progress, but only the root snapshot can "commit".

## The problem

Basically our input is a directed graph where nodes can be divided
Expand Down Expand Up @@ -109,9 +55,9 @@ step where we walk over the verify bounds and check that they are
satisfied. These bounds represent the "maximal" values that a region
variable can take on, basically.

# The Region Hierarchy
## The Region Hierarchy

## Without closures
### Without closures

Let's first consider the region hierarchy without thinking about
closures, because they add a lot of complications. The region
Expand Down Expand Up @@ -141,7 +87,7 @@ Within that, there are sublifetimes for the assignment pattern and
also the expression `x + y`. The expression itself has sublifetimes
for evaluating `x` and `y`.

## Function calls
#s## Function calls

Function calls are a bit tricky. I will describe how we handle them
*now* and then a bit about how we can improve them (Issue #6268).
Expand Down Expand Up @@ -259,7 +205,7 @@ there is a reference created whose lifetime does not enclose
the borrow expression, we must issue sufficient restrictions to ensure
that the pointee remains valid.

## Modeling closures
### Modeling closures

Integrating closures properly into the model is a bit of
work-in-progress. In an ideal world, we would model closures as
Expand Down Expand Up @@ -314,8 +260,3 @@ handling of closures, there are no known cases where this leads to a
type-checking accepting incorrect code (though it sometimes rejects
what might be considered correct code; see rust-lang/rust#22557), but
it still doesn't feel like the right approach.

### Skolemization

For a discussion on skolemization and higher-ranked subtyping, please
see the module `middle::infer::higher_ranked::doc`.
Loading