Auto merge of #56384 - scalexm:chalk, r=nikomatsakis

Implement the new-style trait solver

Final PR of what I believe to be a minimally working implementation of the new-style trait solver.

The new trait solver can be used by providing the `-Z chalk` command line flag. It is currently used everywhere in `rustc_typeck`, and for everything relying on `rustc::infer::canonical::query_response::enter_canonical_trait_query`.

The trait solver is invoked in rustc by using the `evaluate_goal` canonical query. This is not optimal because each call to `evaluate_goal` creates a new `chalk_engine::Forest`, hence rustc cannot use answers to intermediate goals produced by the root goal. We'll need to change that but I guess that's ok for now.

Some next steps, I think, are:
* handle region constraints: region constraints are computed but are completely ignored for now, I think we may need additional support from `chalk_engine` (as a side effect, types or trait references with outlive requirements cannot be proved well-formed)
* deactivate eager normalization in the presence of `-Z chalk` in order to leverage the lazy normalization strategy of the new-style trait solver
* add the remaining built-in impls (only `Sized` is supported currently)
* transition the compiler to using generic goals instead of predicates that still refer to named type parameters etc

I added a few very simple tests to check that the new solver has the right behavior, they won't be needed anymore once it is mature enough. Additionally it shows off that we get [implied bounds](https://github.com/rust-lang/rust/issues/44491) for free.

r? @nikomatsakis

Cargo.lock

@@ -273,7 +273,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 
 [[package]]
 name = "chalk-engine"
-version = "0.8.0"
+version = "0.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 dependencies = [
  "chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -2067,7 +2067,7 @@ dependencies = [
  "backtrace 0.3.11 (registry+https://github.com/rust-lang/crates.io-index)",
  "bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
  "byteorder 1.2.7 (registry+https://github.com/rust-lang/crates.io-index)",
- "chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "chalk-engine 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
  "flate2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
  "fmt_macros 0.0.0",
  "graphviz 0.0.0",
@@ -2640,7 +2640,7 @@ name = "rustc_traits"
 version = "0.0.0"
 dependencies = [
  "bitflags 1.0.4 (registry+https://github.com/rust-lang/crates.io-index)",
- "chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "chalk-engine 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
  "graphviz 0.0.0",
  "log 0.4.6 (registry+https://github.com/rust-lang/crates.io-index)",
  "rustc 0.0.0",
@@ -3403,7 +3403,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 "checksum cargo_metadata 0.6.2 (registry+https://github.com/rust-lang/crates.io-index)" = "7d8dfe3adeb30f7938e6c1dd5327f29235d8ada3e898aeb08c343005ec2915a2"
 "checksum cc 1.0.25 (registry+https://github.com/rust-lang/crates.io-index)" = "f159dfd43363c4d08055a07703eb7a3406b0dac4d0584d96965a3262db3c9d16"
 "checksum cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)" = "082bb9b28e00d3c9d39cc03e64ce4cea0f1bb9b3fde493f0cbc008472d22bdf4"
-"checksum chalk-engine 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)" = "6749eb72e7d4355d944a99f15fbaea701b978c18c5e184a025fcde942b0c9779"
+"checksum chalk-engine 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "17ec698a6f053a23bfbe646d9f2fde4b02abc19125595270a99e6f44ae0bdd1a"
 "checksum chalk-macros 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "295635afd6853aa9f20baeb7f0204862440c0fe994c5a253d5f479dac41d047e"
 "checksum chrono 0.4.6 (registry+https://github.com/rust-lang/crates.io-index)" = "45912881121cb26fad7c38c17ba7daa18764771836b34fab7d3fbd93ed633878"
 "checksum clap 2.32.0 (registry+https://github.com/rust-lang/crates.io-index)" = "b957d88f4b6a63b9d70d5f454ac8011819c6efa7727858f458ab71c756ce2d3e"

src/librustc/Cargo.toml

@@ -30,7 +30,7 @@ syntax_pos = { path = "../libsyntax_pos" }
 backtrace = "0.3.3"
 parking_lot = "0.6"
 byteorder = { version = "1.1", features = ["i128"]}
-chalk-engine = { version = "0.8.0", default-features=false }
+chalk-engine = { version = "0.9.0", default-features=false }
 rustc_fs_util = { path = "../librustc_fs_util" }
 smallvec = { version = "0.6.7", features = ["union", "may_dangle"] }
 

src/librustc/dep_graph/dep_node.rs

@@ -648,6 +648,7 @@ define_dep_nodes!( <'tcx>
     [] ImpliedOutlivesBounds(CanonicalTyGoal<'tcx>),
     [] DropckOutlives(CanonicalTyGoal<'tcx>),
     [] EvaluateObligation(CanonicalPredicateGoal<'tcx>),
+    [] EvaluateGoal(traits::ChalkCanonicalGoal<'tcx>),
     [] TypeOpAscribeUserType(CanonicalTypeOpAscribeUserTypeGoal<'tcx>),
     [] TypeOpEq(CanonicalTypeOpEqGoal<'tcx>),
     [] TypeOpSubtype(CanonicalTypeOpSubtypeGoal<'tcx>),

src/librustc/ich/impls_ty.rs

@@ -885,7 +885,8 @@ for ty::steal::Steal<T>
 
 impl_stable_hash_for!(struct ty::ParamEnv<'tcx> {
     caller_bounds,
-    reveal
+    reveal,
+    def_id
 });
 
 impl_stable_hash_for!(enum traits::Reveal {
@@ -1194,6 +1195,10 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
                 quantifier.hash_stable(hcx, hasher);
                 goal.hash_stable(hcx, hasher);
             },
+            Subtype(a, b) => {
+                a.hash_stable(hcx, hasher);
+                b.hash_stable(hcx, hasher);
+            }
             CannotProve => { },
         }
     }
@@ -1239,3 +1244,10 @@ impl_stable_hash_for!(
         clauses,
     }
 );
+
+impl_stable_hash_for!(
+    impl<'tcx, G> for struct traits::InEnvironment<'tcx, G> {
+        environment,
+        goal,
+    }
+);

src/librustc/infer/canonical/canonicalizer.rs

@@ -330,9 +330,13 @@ impl<'cx, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Canonicalizer<'cx, 'gcx, 'tcx>
     fn fold_ty(&mut self, t: Ty<'tcx>) -> Ty<'tcx> {
         match t.sty {
             ty::Infer(ty::TyVar(vid)) => {
+                debug!("canonical: type var found with vid {:?}", vid);
                 match self.infcx.unwrap().probe_ty_var(vid) {
                     // `t` could be a float / int variable: canonicalize that instead
-                    Ok(t) => self.fold_ty(t),
+                    Ok(t) => {
+                        debug!("(resolved to {:?})", t);
+                        self.fold_ty(t)
+                    }
 
                     // `TyVar(vid)` is unresolved, track its universe index in the canonicalized
                     // result
@@ -448,7 +452,12 @@ impl<'cx, 'gcx, 'tcx> Canonicalizer<'cx, 'gcx, 'tcx> {
 
         // Fast path: nothing that needs to be canonicalized.
         if !value.has_type_flags(needs_canonical_flags) {
-            let out_value = gcx.lift(value).unwrap();
+            let out_value = gcx.lift(value).unwrap_or_else(|| {
+                bug!(
+                    "failed to lift `{:?}` (nothing to canonicalize)",
+                    value
+                )
+            });
             let canon_value = Canonical {
                 max_universe: ty::UniverseIndex::ROOT,
                 variables: List::empty(),

src/librustc/infer/canonical/mod.rs

@@ -420,9 +420,33 @@ BraceStructLiftImpl! {
 }
 
 impl<'tcx> CanonicalVarValues<'tcx> {
-    fn len(&self) -> usize {
+    pub fn len(&self) -> usize {
         self.var_values.len()
     }
+
+    /// Make an identity substitution from this one: each bound var
+    /// is matched to the same bound var, preserving the original kinds.
+    /// For example, if we have:
+    /// `self.var_values == [Type(u32), Lifetime('a), Type(u64)]`
+    /// we'll return a substitution `subst` with:
+    /// `subst.var_values == [Type(^0), Lifetime(^1), Type(^2)]`.
+    pub fn make_identity<'a>(&self, tcx: TyCtxt<'a, 'tcx, 'tcx>) -> Self {
+        use ty::subst::UnpackedKind;
+
+        CanonicalVarValues {
+            var_values: self.var_values.iter()
+                .zip(0..)
+                .map(|(kind, i)| match kind.unpack() {
+                    UnpackedKind::Type(..) => tcx.mk_ty(
+                        ty::Bound(ty::INNERMOST, ty::BoundVar::from_u32(i).into())
+                    ).into(),
+                    UnpackedKind::Lifetime(..) => tcx.mk_region(
+                        ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(i))
+                    ).into(),
+                })
+                .collect()
+        }
+    }
 }
 
 impl<'a, 'tcx> IntoIterator for &'a CanonicalVarValues<'tcx> {

src/librustc/infer/canonical/query_response.rs

@@ -21,7 +21,7 @@ use rustc_data_structures::sync::Lrc;
 use std::fmt::Debug;
 use syntax_pos::DUMMY_SP;
 use traits::query::{Fallible, NoSolution};
-use traits::{FulfillmentContext, TraitEngine};
+use traits::TraitEngine;
 use traits::{Obligation, ObligationCause, PredicateObligation};
 use ty::fold::TypeFoldable;
 use ty::subst::{Kind, UnpackedKind};
@@ -48,7 +48,7 @@ impl<'cx, 'gcx, 'tcx> InferCtxtBuilder<'cx, 'gcx, 'tcx> {
     pub fn enter_canonical_trait_query<K, R>(
         &'tcx mut self,
         canonical_key: &Canonical<'tcx, K>,
-        operation: impl FnOnce(&InferCtxt<'_, 'gcx, 'tcx>, &mut FulfillmentContext<'tcx>, K)
+        operation: impl FnOnce(&InferCtxt<'_, 'gcx, 'tcx>, &mut dyn TraitEngine<'tcx>, K)
             -> Fallible<R>,
     ) -> Fallible<CanonicalizedQueryResponse<'gcx, R>>
     where
@@ -59,9 +59,13 @@ impl<'cx, 'gcx, 'tcx> InferCtxtBuilder<'cx, 'gcx, 'tcx> {
             DUMMY_SP,
             canonical_key,
             |ref infcx, key, canonical_inference_vars| {
-                let fulfill_cx = &mut FulfillmentContext::new();
-                let value = operation(infcx, fulfill_cx, key)?;
-                infcx.make_canonicalized_query_response(canonical_inference_vars, value, fulfill_cx)
+                let mut fulfill_cx = TraitEngine::new(infcx.tcx);
+                let value = operation(infcx, &mut *fulfill_cx, key)?;
+                infcx.make_canonicalized_query_response(
+                    canonical_inference_vars,
+                    value,
+                    &mut *fulfill_cx
+                )
             },
         )
     }
@@ -91,7 +95,7 @@ impl<'cx, 'gcx, 'tcx> InferCtxt<'cx, 'gcx, 'tcx> {
         &self,
         inference_vars: CanonicalVarValues<'tcx>,
         answer: T,
-        fulfill_cx: &mut FulfillmentContext<'tcx>,
+        fulfill_cx: &mut dyn TraitEngine<'tcx>,
     ) -> Fallible<CanonicalizedQueryResponse<'gcx, T>>
     where
         T: Debug + Lift<'gcx> + TypeFoldable<'tcx>,
@@ -138,7 +142,7 @@ impl<'cx, 'gcx, 'tcx> InferCtxt<'cx, 'gcx, 'tcx> {
         &self,
         inference_vars: CanonicalVarValues<'tcx>,
         answer: T,
-        fulfill_cx: &mut FulfillmentContext<'tcx>,
+        fulfill_cx: &mut dyn TraitEngine<'tcx>,
     ) -> Result<QueryResponse<'tcx, T>, NoSolution>
     where
         T: Debug + TypeFoldable<'tcx> + Lift<'gcx>,

src/librustc/infer/mod.rs

@@ -581,7 +581,7 @@ impl<'tcx, T> InferOk<'tcx, T> {
     pub fn into_value_registering_obligations(
         self,
         infcx: &InferCtxt<'_, '_, 'tcx>,
-        fulfill_cx: &mut impl TraitEngine<'tcx>,
+        fulfill_cx: &mut dyn TraitEngine<'tcx>,
     ) -> T {
         let InferOk { value, obligations } = self;
         for obligation in obligations {

src/librustc/traits/auto_trait.rs

@@ -388,12 +388,17 @@ impl<'a, 'tcx> AutoTraitFinder<'a, 'tcx> {
             computed_preds.extend(user_computed_preds.iter().cloned());
             let normalized_preds =
                 elaborate_predicates(tcx, computed_preds.clone().into_iter().collect());
-            new_env = ty::ParamEnv::new(tcx.mk_predicates(normalized_preds), param_env.reveal);
+            new_env = ty::ParamEnv::new(
+                tcx.mk_predicates(normalized_preds),
+                param_env.reveal,
+                None
+            );
         }
 
         let final_user_env = ty::ParamEnv::new(
             tcx.mk_predicates(user_computed_preds.into_iter()),
             user_env.reveal,
+            None
         );
         debug!(
             "evaluate_nested_obligations(ty_did={:?}, trait_did={:?}): succeeded with '{:?}' \

src/librustc/traits/chalk_fulfill.rs

@@ -0,0 +1,165 @@
+use traits::{
+    Environment,
+    InEnvironment,
+    TraitEngine,
+    ObligationCause,
+    PredicateObligation,
+    FulfillmentError,
+    FulfillmentErrorCode,
+    SelectionError,
+};
+use traits::query::NoSolution;
+use infer::InferCtxt;
+use infer::canonical::{Canonical, OriginalQueryValues};
+use ty::{self, Ty};
+use rustc_data_structures::fx::FxHashSet;
+
+pub type CanonicalGoal<'tcx> = Canonical<'tcx, InEnvironment<'tcx, ty::Predicate<'tcx>>>;
+
+pub struct FulfillmentContext<'tcx> {
+    obligations: FxHashSet<InEnvironment<'tcx, PredicateObligation<'tcx>>>,
+}
+
+impl FulfillmentContext<'tcx> {
+    crate fn new() -> Self {
+        FulfillmentContext {
+            obligations: FxHashSet::default(),
+        }
+    }
+}
+
+fn in_environment(
+    infcx: &InferCtxt<'_, 'gcx, 'tcx>,
+    obligation: PredicateObligation<'tcx>
+) -> InEnvironment<'tcx, PredicateObligation<'tcx>> {
+    assert!(!infcx.is_in_snapshot());
+    let obligation = infcx.resolve_type_vars_if_possible(&obligation);
+
+    let environment = match obligation.param_env.def_id {
+        Some(def_id) => infcx.tcx.environment(def_id),
+        None if obligation.param_env.caller_bounds.is_empty() => Environment {
+            clauses: ty::List::empty(),
+        },
+        _ => bug!("non-empty `ParamEnv` with no def-id"),
+    };
+
+    InEnvironment {
+        environment,
+        goal: obligation,
+    }
+}
+
+impl TraitEngine<'tcx> for FulfillmentContext<'tcx> {
+    fn normalize_projection_type(
+        &mut self,
+        infcx: &InferCtxt<'_, 'gcx, 'tcx>,
+        _param_env: ty::ParamEnv<'tcx>,
+        projection_ty: ty::ProjectionTy<'tcx>,
+        _cause: ObligationCause<'tcx>,
+    ) -> Ty<'tcx> {
+        infcx.tcx.mk_ty(ty::Projection(projection_ty))
+    }
+
+    fn register_predicate_obligation(
+        &mut self,
+        infcx: &InferCtxt<'_, 'gcx, 'tcx>,
+        obligation: PredicateObligation<'tcx>,
+    ) {
+        self.obligations.insert(in_environment(infcx, obligation));
+    }
+
+    fn select_all_or_error(
+        &mut self,
+        infcx: &InferCtxt<'_, 'gcx, 'tcx>,
+    ) -> Result<(), Vec<FulfillmentError<'tcx>>> {
+        self.select_where_possible(infcx)?;
+
+        if self.obligations.is_empty() {
+            Ok(())
+        } else {
+            let errors = self.obligations.iter()
+                .map(|obligation| FulfillmentError {
+                    obligation: obligation.goal.clone(),
+                    code: FulfillmentErrorCode::CodeAmbiguity,
+                })
+                .collect();
+            Err(errors)
+        }
+    }
+
+    fn select_where_possible(
+        &mut self,
+        infcx: &InferCtxt<'_, 'gcx, 'tcx>,
+    ) -> Result<(), Vec<FulfillmentError<'tcx>>> {
+        let mut errors = Vec::new();
+        let mut next_round = FxHashSet::default();
+        let mut making_progress;
+
+        loop {
+            making_progress = false;
+
+            // We iterate over all obligations, and record if we are able
+            // to unambiguously prove at least one obligation.
+            for obligation in self.obligations.drain() {
+                let mut orig_values = OriginalQueryValues::default();
+                let canonical_goal = infcx.canonicalize_query(&InEnvironment {
+                    environment: obligation.environment,
+                    goal: obligation.goal.predicate,
+                }, &mut orig_values);
+
+                match infcx.tcx.global_tcx().evaluate_goal(canonical_goal) {
+                    Ok(response) => {
+                        if response.is_proven() {
+                            making_progress = true;
+
+                            match infcx.instantiate_query_response_and_region_obligations(
+                                &obligation.goal.cause,
+                                obligation.goal.param_env,
+                                &orig_values,
+                                &response
+                            ) {
+                                Ok(infer_ok) => next_round.extend(
+                                    infer_ok.obligations
+                                        .into_iter()
+                                        .map(|obligation| in_environment(infcx, obligation))
+                                ),
+
+                                Err(_err) => errors.push(FulfillmentError {
+                                    obligation: obligation.goal,
+                                    code: FulfillmentErrorCode::CodeSelectionError(
+                                        SelectionError::Unimplemented
+                                    ),
+                                }),
+                            }
+                        } else {
+                            // Ambiguous: retry at next round.
+                            next_round.insert(obligation);
+                        }
+                    }
+
+                    Err(NoSolution) => errors.push(FulfillmentError {
+                        obligation: obligation.goal,
+                        code: FulfillmentErrorCode::CodeSelectionError(
+                            SelectionError::Unimplemented
+                        ),
+                    })
+                }
+            }
+            next_round = std::mem::replace(&mut self.obligations, next_round);
+
+            if !making_progress {
+                break;
+            }
+        }
+
+        if errors.is_empty() {
+            Ok(())
+        } else {
+            Err(errors)
+        }
+    }
+
+    fn pending_obligations(&self) -> Vec<PredicateObligation<'tcx>> {
+        self.obligations.iter().map(|obligation| obligation.goal.clone()).collect()
+    }
+}

src/librustc/traits/engine.rs

@@ -1,8 +1,9 @@
 use infer::InferCtxt;
-use ty::{self, Ty, TyCtxt};
+use ty::{self, Ty, TyCtxt, ToPredicate};
+use traits::Obligation;
 use hir::def_id::DefId;
 
-use super::{FulfillmentContext, FulfillmentError};
+use super::{ChalkFulfillmentContext, FulfillmentContext, FulfillmentError};
 use super::{ObligationCause, PredicateObligation};
 
 pub trait TraitEngine<'tcx>: 'tcx {
@@ -14,6 +15,9 @@ pub trait TraitEngine<'tcx>: 'tcx {
         cause: ObligationCause<'tcx>,
     ) -> Ty<'tcx>;
 
+    /// Requires that `ty` must implement the trait with `def_id` in
+    /// the given environment. This trait must not have any type
+    /// parameters (except for `Self`).
     fn register_bound(
         &mut self,
         infcx: &InferCtxt<'_, 'gcx, 'tcx>,
@@ -21,7 +25,18 @@ pub trait TraitEngine<'tcx>: 'tcx {
         ty: Ty<'tcx>,
         def_id: DefId,
         cause: ObligationCause<'tcx>,
-    );
+    ) {
+        let trait_ref = ty::TraitRef {
+            def_id,
+            substs: infcx.tcx.mk_substs_trait(ty, &[]),
+        };
+        self.register_predicate_obligation(infcx, Obligation {
+            cause,
+            recursion_depth: 0,
+            param_env,
+            predicate: trait_ref.to_predicate()
+        });
+    }
 
     fn register_predicate_obligation(
         &mut self,
@@ -63,7 +78,11 @@ impl<T: ?Sized + TraitEngine<'tcx>> TraitEngineExt<'tcx> for T {
 }
 
 impl dyn TraitEngine<'tcx> {
-    pub fn new(_tcx: TyCtxt<'_, '_, 'tcx>) -> Box<Self> {
-        Box::new(FulfillmentContext::new())
+    pub fn new(tcx: TyCtxt<'_, '_, 'tcx>) -> Box<Self> {
+        if tcx.sess.opts.debugging_opts.chalk {
+            Box::new(ChalkFulfillmentContext::new())
+        } else {
+            Box::new(FulfillmentContext::new())
+        }
     }
 }

src/librustc/traits/error_reporting.rs

@@ -796,12 +796,21 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
                     }
 
                     ty::Predicate::WellFormed(ty) => {
-                        // WF predicates cannot themselves make
-                        // errors. They can only block due to
-                        // ambiguity; otherwise, they always
-                        // degenerate into other obligations
-                        // (which may fail).
-                        span_bug!(span, "WF predicate not satisfied for {:?}", ty);
+                        if !self.tcx.sess.opts.debugging_opts.chalk {
+                            // WF predicates cannot themselves make
+                            // errors. They can only block due to
+                            // ambiguity; otherwise, they always
+                            // degenerate into other obligations
+                            // (which may fail).
+                            span_bug!(span, "WF predicate not satisfied for {:?}", ty);
+                        } else {
+                            // FIXME: we'll need a better message which takes into account
+                            // which bounds actually failed to hold.
+                            self.tcx.sess.struct_span_err(
+                                span,
+                                &format!("the type `{}` is not well-formed (chalk)", ty)
+                            )
+                        }
                     }
 
                     ty::Predicate::ConstEvaluatable(..) => {

src/librustc/traits/fulfill.rs

@@ -1,19 +1,18 @@
 use infer::InferCtxt;
 use mir::interpret::{GlobalId, ErrorHandled};
-use ty::{self, Ty, TypeFoldable, ToPolyTraitRef, ToPredicate};
+use ty::{self, Ty, TypeFoldable, ToPolyTraitRef};
 use ty::error::ExpectedFound;
 use rustc_data_structures::obligation_forest::{DoCompleted, Error, ForestObligation};
 use rustc_data_structures::obligation_forest::{ObligationForest, ObligationProcessor};
 use rustc_data_structures::obligation_forest::{ProcessResult};
 use std::marker::PhantomData;
-use hir::def_id::DefId;
 
 use super::CodeAmbiguity;
 use super::CodeProjectionError;
 use super::CodeSelectionError;
 use super::engine::{TraitEngine, TraitEngineExt};
 use super::{FulfillmentError, FulfillmentErrorCode};
-use super::{ObligationCause, PredicateObligation, Obligation};
+use super::{ObligationCause, PredicateObligation};
 use super::project;
 use super::select::SelectionContext;
 use super::{Unimplemented, ConstEvalFailure};
@@ -173,28 +172,6 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentContext<'tcx> {
         normalized_ty
     }
 
-    /// Requires that `ty` must implement the trait with `def_id` in
-    /// the given environment. This trait must not have any type
-    /// parameters (except for `Self`).
-    fn register_bound<'a, 'gcx>(&mut self,
-                      infcx: &InferCtxt<'a, 'gcx, 'tcx>,
-                      param_env: ty::ParamEnv<'tcx>,
-                      ty: Ty<'tcx>,
-                      def_id: DefId,
-                      cause: ObligationCause<'tcx>)
-    {
-        let trait_ref = ty::TraitRef {
-            def_id,
-            substs: infcx.tcx.mk_substs_trait(ty, &[]),
-        };
-        self.register_predicate_obligation(infcx, Obligation {
-            cause,
-            recursion_depth: 0,
-            param_env,
-            predicate: trait_ref.to_predicate()
-        });
-    }
-
     fn register_predicate_obligation<'a, 'gcx>(&mut self,
                                      infcx: &InferCtxt<'a, 'gcx, 'tcx>,
                                      obligation: PredicateObligation<'tcx>)
@@ -213,9 +190,10 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentContext<'tcx> {
         });
     }
 
-    fn select_all_or_error<'a, 'gcx>(&mut self,
-                                     infcx: &InferCtxt<'a, 'gcx, 'tcx>)
-                                     -> Result<(),Vec<FulfillmentError<'tcx>>>
+    fn select_all_or_error<'a, 'gcx>(
+        &mut self,
+        infcx: &InferCtxt<'a, 'gcx, 'tcx>
+    ) -> Result<(),Vec<FulfillmentError<'tcx>>>
     {
         self.select_where_possible(infcx)?;
 

src/librustc/traits/mod.rs

@@ -4,6 +4,7 @@
 
 #[allow(dead_code)]
 pub mod auto_trait;
+mod chalk_fulfill;
 mod coherence;
 pub mod error_reporting;
 mod engine;
@@ -61,6 +62,11 @@ pub use self::util::{elaborate_predicates, elaborate_trait_ref, elaborate_trait_
 pub use self::util::{supertraits, supertrait_def_ids, transitive_bounds,
                      Supertraits, SupertraitDefIds};
 
+pub use self::chalk_fulfill::{
+    CanonicalGoal as ChalkCanonicalGoal,
+    FulfillmentContext as ChalkFulfillmentContext
+};
+
 pub use self::ObligationCauseCode::*;
 pub use self::FulfillmentErrorCode::*;
 pub use self::SelectionError::*;
@@ -318,6 +324,7 @@ pub enum GoalKind<'tcx> {
     Not(Goal<'tcx>),
     DomainGoal(DomainGoal<'tcx>),
     Quantified(QuantifierKind, ty::Binder<Goal<'tcx>>),
+    Subtype(Ty<'tcx>, Ty<'tcx>),
     CannotProve,
 }
 
@@ -340,9 +347,9 @@ impl<'tcx> DomainGoal<'tcx> {
 }
 
 impl<'tcx> GoalKind<'tcx> {
-    pub fn from_poly_domain_goal<'a>(
+    pub fn from_poly_domain_goal<'a, 'gcx>(
         domain_goal: PolyDomainGoal<'tcx>,
-        tcx: TyCtxt<'a, 'tcx, 'tcx>,
+        tcx: TyCtxt<'a, 'gcx, 'tcx>,
     ) -> GoalKind<'tcx> {
         match domain_goal.no_bound_vars() {
             Some(p) => p.into_goal(),
@@ -804,8 +811,11 @@ pub fn normalize_param_env_or_error<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     debug!("normalize_param_env_or_error: elaborated-predicates={:?}",
            predicates);
 
-    let elaborated_env = ty::ParamEnv::new(tcx.intern_predicates(&predicates),
-                                           unnormalized_env.reveal);
+    let elaborated_env = ty::ParamEnv::new(
+        tcx.intern_predicates(&predicates),
+        unnormalized_env.reveal,
+        unnormalized_env.def_id
+    );
 
     // HACK: we are trying to normalize the param-env inside *itself*. The problem is that
     // normalization expects its param-env to be already normalized, which means we have
@@ -852,8 +862,11 @@ pub fn normalize_param_env_or_error<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     // predicates here anyway. Keeping them here anyway because it seems safer.
     let outlives_env: Vec<_> =
         non_outlives_predicates.iter().chain(&outlives_predicates).cloned().collect();
-    let outlives_env = ty::ParamEnv::new(tcx.intern_predicates(&outlives_env),
-                                         unnormalized_env.reveal);
+    let outlives_env = ty::ParamEnv::new(
+        tcx.intern_predicates(&outlives_env),
+        unnormalized_env.reveal,
+        None
+    );
     let outlives_predicates =
         match do_normalize_predicates(tcx, region_context, cause,
                                       outlives_env, outlives_predicates) {
@@ -869,7 +882,11 @@ pub fn normalize_param_env_or_error<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     let mut predicates = non_outlives_predicates;
     predicates.extend(outlives_predicates);
     debug!("normalize_param_env_or_error: final predicates={:?}", predicates);
-    ty::ParamEnv::new(tcx.intern_predicates(&predicates), unnormalized_env.reveal)
+    ty::ParamEnv::new(
+        tcx.intern_predicates(&predicates),
+        unnormalized_env.reveal,
+        unnormalized_env.def_id
+    )
 }
 
 pub fn fully_normalize<'a, 'gcx, 'tcx, T>(
@@ -1164,14 +1181,26 @@ where
     ) -> bool;
 }
 
-pub trait ExClauseLift<'tcx>
+pub trait ChalkContextLift<'tcx>
 where
     Self: chalk_engine::context::Context + Clone,
 {
     type LiftedExClause: Debug + 'tcx;
+    type LiftedDelayedLiteral: Debug + 'tcx;
+    type LiftedLiteral: Debug + 'tcx;
 
     fn lift_ex_clause_to_tcx<'a, 'gcx>(
         ex_clause: &chalk_engine::ExClause<Self>,
         tcx: TyCtxt<'a, 'gcx, 'tcx>,
     ) -> Option<Self::LiftedExClause>;
+
+    fn lift_delayed_literal_to_tcx<'a, 'gcx>(
+        ex_clause: &chalk_engine::DelayedLiteral<Self>,
+        tcx: TyCtxt<'a, 'gcx, 'tcx>,
+    ) -> Option<Self::LiftedDelayedLiteral>;
+
+    fn lift_literal_to_tcx<'a, 'gcx>(
+        ex_clause: &chalk_engine::Literal<Self>,
+        tcx: TyCtxt<'a, 'gcx, 'tcx>,
+    ) -> Option<Self::LiftedLiteral>;
 }

src/librustc/traits/select.rs

@@ -3243,11 +3243,14 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
             trait_ref,
         )?);
 
-        obligations.push(Obligation::new(
-            obligation.cause.clone(),
-            obligation.param_env,
-            ty::Predicate::ClosureKind(closure_def_id, substs, kind),
-        ));
+        // FIXME: chalk
+        if !self.tcx().sess.opts.debugging_opts.chalk {
+            obligations.push(Obligation::new(
+                obligation.cause.clone(),
+                obligation.param_env,
+                ty::Predicate::ClosureKind(closure_def_id, substs, kind),
+            ));
+        }
 
         Ok(VtableClosureData {
             closure_def_id,

src/librustc/traits/structural_impls.rs

@@ -395,6 +395,7 @@ impl<'tcx> fmt::Display for traits::Goal<'tcx> {
 
                 Ok(())
             }
+            Subtype(a, b) => write!(fmt, "{} <: {}", a, b),
             CannotProve => write!(fmt, "CannotProve"),
         }
     }
@@ -668,6 +669,7 @@ EnumLiftImpl! {
         (traits::GoalKind::Not)(goal),
         (traits::GoalKind::DomainGoal)(domain_goal),
         (traits::GoalKind::Quantified)(kind, goal),
+        (traits::GoalKind::Subtype)(a, b),
         (traits::GoalKind::CannotProve),
     }
 }
@@ -700,12 +702,36 @@ impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
 impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
 where
     C: chalk_engine::context::Context + Clone,
-    C: traits::ExClauseLift<'tcx>,
+    C: traits::ChalkContextLift<'tcx>,
 {
     type Lifted = C::LiftedExClause;
 
     fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
-        <C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
+        <C as traits::ChalkContextLift>::lift_ex_clause_to_tcx(self, tcx)
+    }
+}
+
+impl<'tcx, C> Lift<'tcx> for chalk_engine::DelayedLiteral<C>
+where
+    C: chalk_engine::context::Context + Clone,
+    C: traits::ChalkContextLift<'tcx>,
+{
+    type Lifted = C::LiftedDelayedLiteral;
+
+    fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+        <C as traits::ChalkContextLift>::lift_delayed_literal_to_tcx(self, tcx)
+    }
+}
+
+impl<'tcx, C> Lift<'tcx> for chalk_engine::Literal<C>
+where
+    C: chalk_engine::context::Context + Clone,
+    C: traits::ChalkContextLift<'tcx>,
+{
+    type Lifted = C::LiftedLiteral;
+
+    fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+        <C as traits::ChalkContextLift>::lift_literal_to_tcx(self, tcx)
     }
 }
 
@@ -840,6 +866,7 @@ EnumTypeFoldableImpl! {
         (traits::GoalKind::Not)(goal),
         (traits::GoalKind::DomainGoal)(domain_goal),
         (traits::GoalKind::Quantified)(qkind, goal),
+        (traits::GoalKind::Subtype)(a, b),
         (traits::GoalKind::CannotProve),
     }
 }

src/librustc/ty/context.rs

@@ -1714,6 +1714,10 @@ impl<'a, 'tcx> Lift<'tcx> for &'a List<Goal<'a>> {
         &self,
         tcx: TyCtxt<'b, 'gcx, 'tcx>,
     ) -> Option<&'tcx List<Goal<'tcx>>> {
+        if self.is_empty() {
+            return Some(List::empty());
+        }
+
         if tcx.interners.arena.in_arena(*self as *const _) {
             return Some(unsafe { mem::transmute(*self) });
         }
@@ -1732,6 +1736,10 @@ impl<'a, 'tcx> Lift<'tcx> for &'a List<Clause<'a>> {
         &self,
         tcx: TyCtxt<'b, 'gcx, 'tcx>,
     ) -> Option<&'tcx List<Clause<'tcx>>> {
+        if self.is_empty() {
+            return Some(List::empty());
+        }
+
         if tcx.interners.arena.in_arena(*self as *const _) {
             return Some(unsafe { mem::transmute(*self) });
         }

src/librustc/ty/fold.rs

@@ -533,18 +533,25 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
               G: FnMut(ty::BoundTy) -> ty::Ty<'tcx>,
               T: TypeFoldable<'tcx>
     {
-        let mut map = BTreeMap::new();
+        use rustc_data_structures::fx::FxHashMap;
+
+        let mut region_map = BTreeMap::new();
+        let mut type_map = FxHashMap::default();
 
         if !value.has_escaping_bound_vars() {
-            (value.clone(), map)
+            (value.clone(), region_map)
         } else {
             let mut real_fld_r = |br| {
-                *map.entry(br).or_insert_with(|| fld_r(br))
+                *region_map.entry(br).or_insert_with(|| fld_r(br))
             };
 
-            let mut replacer = BoundVarReplacer::new(self, &mut real_fld_r, &mut fld_t);
+            let mut real_fld_t = |bound_ty| {
+                *type_map.entry(bound_ty).or_insert_with(|| fld_t(bound_ty))
+            };
+
+            let mut replacer = BoundVarReplacer::new(self, &mut real_fld_r, &mut real_fld_t);
             let result = value.fold_with(&mut replacer);
-            (result, map)
+            (result, region_map)
         }
     }
 

src/librustc/ty/mod.rs

@@ -1617,6 +1617,11 @@ pub struct ParamEnv<'tcx> {
     /// want `Reveal::All` -- note that this is always paired with an
     /// empty environment. To get that, use `ParamEnv::reveal()`.
     pub reveal: traits::Reveal,
+
+    /// If this `ParamEnv` comes from a call to `tcx.param_env(def_id)`,
+    /// register that `def_id` (useful for transitioning to the chalk trait
+    /// solver).
+    pub def_id: Option<DefId>,
 }
 
 impl<'tcx> ParamEnv<'tcx> {
@@ -1626,7 +1631,7 @@ impl<'tcx> ParamEnv<'tcx> {
     /// type-checking.
     #[inline]
     pub fn empty() -> Self {
-        Self::new(List::empty(), Reveal::UserFacing)
+        Self::new(List::empty(), Reveal::UserFacing, None)
     }
 
     /// Construct a trait environment with no where clauses in scope
@@ -1638,15 +1643,17 @@ impl<'tcx> ParamEnv<'tcx> {
     /// or invoke `param_env.with_reveal_all()`.
     #[inline]
     pub fn reveal_all() -> Self {
-        Self::new(List::empty(), Reveal::All)
+        Self::new(List::empty(), Reveal::All, None)
     }
 
     /// Construct a trait environment with the given set of predicates.
     #[inline]
-    pub fn new(caller_bounds: &'tcx List<ty::Predicate<'tcx>>,
-               reveal: Reveal)
-               -> Self {
-        ty::ParamEnv { caller_bounds, reveal }
+    pub fn new(
+        caller_bounds: &'tcx List<ty::Predicate<'tcx>>,
+        reveal: Reveal,
+        def_id: Option<DefId>
+    ) -> Self {
+        ty::ParamEnv { caller_bounds, reveal, def_id }
     }
 
     /// Returns a new parameter environment with the same clauses, but
@@ -3148,8 +3155,11 @@ fn param_env<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     // are any errors at that point, so after type checking you can be
     // sure that this will succeed without errors anyway.
 
-    let unnormalized_env = ty::ParamEnv::new(tcx.intern_predicates(&predicates),
-                                             traits::Reveal::UserFacing);
+    let unnormalized_env = ty::ParamEnv::new(
+        tcx.intern_predicates(&predicates),
+        traits::Reveal::UserFacing,
+        if tcx.sess.opts.debugging_opts.chalk { Some(def_id) } else { None }
+    );
 
     let body_id = tcx.hir().as_local_node_id(def_id).map_or(DUMMY_NODE_ID, |id| {
         tcx.hir().maybe_body_owned_by(id).map_or(id, |body| body.node_id)

src/librustc/ty/query/config.rs

@@ -106,6 +106,15 @@ impl<'tcx> QueryDescription<'tcx> for queries::evaluate_obligation<'tcx> {
     }
 }
 
+impl<'tcx> QueryDescription<'tcx> for queries::evaluate_goal<'tcx> {
+    fn describe(
+        _tcx: TyCtxt<'_, '_, '_>,
+        goal: traits::ChalkCanonicalGoal<'tcx>
+    ) -> Cow<'static, str> {
+        format!("evaluating trait selection obligation `{}`", goal.value.goal).into()
+    }
+}
+
 impl<'tcx> QueryDescription<'tcx> for queries::type_op_ascribe_user_type<'tcx> {
     fn describe(
         _tcx: TyCtxt<'_, '_, '_>,

src/librustc/ty/query/mod.rs

@@ -593,6 +593,13 @@ define_queries! { <'tcx>
             CanonicalPredicateGoal<'tcx>
         ) -> Result<traits::EvaluationResult, traits::OverflowError>,
 
+        [] fn evaluate_goal: EvaluateGoal(
+            traits::ChalkCanonicalGoal<'tcx>
+        ) -> Result<
+            Lrc<Canonical<'tcx, canonical::QueryResponse<'tcx, ()>>>,
+            NoSolution
+        >,
+
         /// Do not call this query directly: part of the `Eq` type-op
         [] fn type_op_ascribe_user_type: TypeOpAscribeUserType(
             CanonicalTypeOpAscribeUserTypeGoal<'tcx>
@@ -684,7 +691,7 @@ define_queries! { <'tcx>
         ) -> Clauses<'tcx>,
 
         // Get the chalk-style environment of the given item.
-        [] fn environment: Environment(DefId) -> ty::Binder<traits::Environment<'tcx>>,
+        [] fn environment: Environment(DefId) -> traits::Environment<'tcx>,
     },
 
     Linking {

src/librustc/ty/query/plumbing.rs

@@ -1103,6 +1103,7 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
         DepKind::ImpliedOutlivesBounds |
         DepKind::DropckOutlives |
         DepKind::EvaluateObligation |
+        DepKind::EvaluateGoal |
         DepKind::TypeOpAscribeUserType |
         DepKind::TypeOpEq |
         DepKind::TypeOpSubtype |

src/librustc/ty/structural_impls.rs

@@ -276,6 +276,7 @@ impl<'a, 'tcx> Lift<'tcx> for ty::ParamEnv<'a> {
             ty::ParamEnv {
                 reveal: self.reveal,
                 caller_bounds,
+                def_id: self.def_id,
             }
         })
     }
@@ -589,7 +590,7 @@ impl<'tcx, T:TypeFoldable<'tcx>> TypeFoldable<'tcx> for ty::Binder<T> {
 }
 
 BraceStructTypeFoldableImpl! {
-    impl<'tcx> TypeFoldable<'tcx> for ty::ParamEnv<'tcx> { reveal, caller_bounds }
+    impl<'tcx> TypeFoldable<'tcx> for ty::ParamEnv<'tcx> { reveal, caller_bounds, def_id }
 }
 
 impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::List<ty::ExistentialPredicate<'tcx>> {

src/librustc_traits/Cargo.toml

@@ -17,5 +17,5 @@ rustc_data_structures = { path = "../librustc_data_structures" }
 rustc_target = { path = "../librustc_target" }
 syntax = { path = "../libsyntax" }
 syntax_pos = { path = "../libsyntax_pos" }
-chalk-engine = { version = "0.8.0", default-features=false }
+chalk-engine = { version = "0.9.0", default-features=false }
 smallvec = { version = "0.6.7", features = ["union", "may_dangle"] }

src/librustc_traits/chalk_context/mod.rs

@@ -2,14 +2,15 @@ mod program_clauses;
 mod resolvent_ops;
 mod unify;
 
-use chalk_engine::fallible::{Fallible, NoSolution};
+use chalk_engine::fallible::Fallible;
 use chalk_engine::{
     context,
     hh::HhGoal,
     DelayedLiteral,
     Literal,
-    ExClause
+    ExClause,
 };
+use chalk_engine::forest::Forest;
 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
 use rustc::infer::canonical::{
     Canonical,
@@ -19,19 +20,23 @@ use rustc::infer::canonical::{
     Certainty,
 };
 use rustc::traits::{
+    self,
     DomainGoal,
     ExClauseFold,
-    ExClauseLift,
+    ChalkContextLift,
     Goal,
     GoalKind,
     Clause,
     QuantifierKind,
     Environment,
     InEnvironment,
+    ChalkCanonicalGoal,
 };
 use rustc::ty::{self, TyCtxt};
 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
+use rustc::ty::query::Providers;
 use rustc::ty::subst::{Kind, UnpackedKind};
+use rustc_data_structures::sync::Lrc;
 use syntax_pos::DUMMY_SP;
 
 use std::fmt::{self, Debug};
@@ -111,6 +116,8 @@ impl context::Context for ChalkArenas<'tcx> {
 
     type UnificationResult = UnificationResult<'tcx>;
 
+    type Variance = ty::Variance;
+
     fn goal_in_environment(
         env: &Environment<'tcx>,
         goal: Goal<'tcx>,
@@ -122,45 +129,77 @@ impl context::Context for ChalkArenas<'tcx> {
 impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
     fn make_solution(
         &self,
-        _root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
+        root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
         mut simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
     ) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
         use chalk_engine::SimplifiedAnswer;
 
+        debug!("make_solution(root_goal = {:?})", root_goal);
+
         if simplified_answers.peek_answer().is_none() {
             return None;
         }
 
-        let SimplifiedAnswer { subst, ambiguous } = simplified_answers
+        let SimplifiedAnswer { subst: constrained_subst, ambiguous } = simplified_answers
             .next_answer()
             .unwrap();
 
+        debug!("make_solution: ambiguous flag = {}", ambiguous);
+
         let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
 
-        Some(subst.unchecked_map(|subst| {
-            QueryResponse {
-                var_values: subst.subst,
-                region_constraints: subst.constraints
-                    .into_iter()
-                    .map(|c| ty::Binder::bind(c))
-                    .collect(),
-                certainty: match ambiguous {
-                    true => Certainty::Ambiguous,
-                    false => Certainty::Proven,
-                },
+        let solution = constrained_subst.unchecked_map(|cs| match ambiguous {
+            true => QueryResponse {
+                var_values: cs.subst.make_identity(self.tcx),
+                region_constraints: Vec::new(),
+                certainty: Certainty::Ambiguous,
                 value: (),
-            }
-        }))
+            },
+
+            false => QueryResponse {
+                var_values: cs.subst,
+                region_constraints: Vec::new(),
+
+                // FIXME: restore this later once we get better at handling regions
+                // region_constraints: cs.constraints
+                //     .into_iter()
+                //     .map(|c| ty::Binder::bind(c))
+                //     .collect(),
+                certainty: Certainty::Proven,
+                value: (),
+            },
+        });
+
+        debug!("make_solution: solution = {:?}", solution);
+
+        Some(solution)
     }
 }
 
 impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
-    /// True if this is a coinductive goal -- e.g., proving an auto trait.
+    /// True if this is a coinductive goal: basically proving that an auto trait
+    /// is implemented or proving that a trait reference is well-formed.
     fn is_coinductive(
         &self,
-        _goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
+        goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
     ) -> bool {
-        unimplemented!()
+        use rustc::traits::{WellFormed, WhereClause};
+
+        let mut goal = goal.value.goal;
+        loop {
+            match goal {
+                GoalKind::DomainGoal(domain_goal) => match domain_goal {
+                    DomainGoal::WellFormed(WellFormed::Trait(..)) => return true,
+                    DomainGoal::Holds(WhereClause::Implemented(trait_predicate)) => {
+                        return self.tcx.trait_is_auto(trait_predicate.def_id());
+                    }
+                    _ => return false,
+                }
+
+                GoalKind::Quantified(_, bound_goal) => goal = *bound_goal.skip_binder(),
+                _ => return false,
+            }
+        }
     }
 
     /// Create an inference table for processing a new goal and instantiate that goal
@@ -295,6 +334,11 @@ impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
             GoalKind::DomainGoal(d) => HhGoal::DomainGoal(d),
             GoalKind::Quantified(QuantifierKind::Universal, binder) => HhGoal::ForAll(binder),
             GoalKind::Quantified(QuantifierKind::Existential, binder) => HhGoal::Exists(binder),
+            GoalKind::Subtype(a, b) => HhGoal::Unify(
+                ty::Variance::Covariant,
+                a.into(),
+                b.into()
+            ),
             GoalKind::CannotProve => HhGoal::CannotProve,
         }
     }
@@ -317,16 +361,16 @@ impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 {
     fn truncate_goal(
         &mut self,
-        subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
+        _subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
     ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
-        Some(*subgoal) // FIXME we should truncate at some point!
+        None // FIXME we should truncate at some point!
     }
 
     fn truncate_answer(
         &mut self,
-        subst: &CanonicalVarValues<'tcx>,
+        _subst: &CanonicalVarValues<'tcx>,
     ) -> Option<CanonicalVarValues<'tcx>> {
-        Some(subst.clone()) // FIXME we should truncate at some point!
+        None // FIXME we should truncate at some point!
     }
 }
 
@@ -407,11 +451,13 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     fn unify_parameters(
         &mut self,
         environment: &Environment<'tcx>,
+        variance: ty::Variance,
         a: &Kind<'tcx>,
         b: &Kind<'tcx>,
     ) -> Fallible<UnificationResult<'tcx>> {
         self.infcx.commit_if_ok(|_| {
-            unify(self.infcx, *environment, a, b).map_err(|_| NoSolution)
+            unify(self.infcx, *environment, variance, a, b)
+                .map_err(|_| chalk_engine::fallible::NoSolution)
         })
     }
 
@@ -424,9 +470,12 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 
     fn lift_delayed_literal(
         &self,
-        _value: DelayedLiteral<ChalkArenas<'tcx>>,
+        value: DelayedLiteral<ChalkArenas<'tcx>>,
     ) -> DelayedLiteral<ChalkArenas<'gcx>> {
-        panic!("lift")
+        match self.infcx.tcx.lift_to_global(&value) {
+            Some(literal) => literal,
+            None => bug!("cannot lift {:?}", value),
+        }
     }
 
     fn into_ex_clause(
@@ -442,7 +491,10 @@ crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkEx
     ex_clause.subgoals.extend(
         result.goals.into_iter().map(Literal::Positive)
     );
-    ex_clause.constraints.extend(result.constraints);
+
+    // FIXME: restore this later once we get better at handling regions
+    let _ = result.constraints.len(); // trick `-D dead-code`
+    // ex_clause.constraints.extend(result.constraints);
 }
 
 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
@@ -461,14 +513,45 @@ impl Debug for ChalkInferenceContext<'cx, 'gcx, 'tcx> {
     }
 }
 
-impl ExClauseLift<'gcx> for ChalkArenas<'a> {
-    type LiftedExClause = ChalkExClause<'gcx>;
+impl ChalkContextLift<'tcx> for ChalkArenas<'a> {
+    type LiftedExClause = ChalkExClause<'tcx>;
+    type LiftedDelayedLiteral = DelayedLiteral<ChalkArenas<'tcx>>;
+    type LiftedLiteral = Literal<ChalkArenas<'tcx>>;
 
     fn lift_ex_clause_to_tcx(
-        _ex_clause: &ChalkExClause<'a>,
-        _tcx: TyCtxt<'_, '_, 'tcx>,
+        ex_clause: &ChalkExClause<'a>,
+        tcx: TyCtxt<'_, 'gcx, 'tcx>
     ) -> Option<Self::LiftedExClause> {
-        panic!()
+        Some(ChalkExClause {
+            subst: tcx.lift(&ex_clause.subst)?,
+            delayed_literals: tcx.lift(&ex_clause.delayed_literals)?,
+            constraints: tcx.lift(&ex_clause.constraints)?,
+            subgoals: tcx.lift(&ex_clause.subgoals)?,
+        })
+    }
+
+    fn lift_delayed_literal_to_tcx(
+        literal: &DelayedLiteral<ChalkArenas<'a>>,
+        tcx: TyCtxt<'_, 'gcx, 'tcx>
+    ) -> Option<Self::LiftedDelayedLiteral> {
+        Some(match literal {
+            DelayedLiteral::CannotProve(()) => DelayedLiteral::CannotProve(()),
+            DelayedLiteral::Negative(index) => DelayedLiteral::Negative(*index),
+            DelayedLiteral::Positive(index, subst) => DelayedLiteral::Positive(
+                *index,
+                tcx.lift(subst)?
+            )
+        })
+    }
+
+    fn lift_literal_to_tcx(
+        literal: &Literal<ChalkArenas<'a>>,
+        tcx: TyCtxt<'_, 'gcx, 'tcx>,
+    ) -> Option<Self::LiftedLiteral> {
+        Some(match literal {
+            Literal::Negative(goal) => Literal::Negative(tcx.lift(goal)?),
+            Literal::Positive(goal) =>  Literal::Positive(tcx.lift(goal)?),
+        })
     }
 }
 
@@ -496,9 +579,9 @@ impl ExClauseFold<'tcx> for ChalkArenas<'tcx> {
             subgoals,
         } = ex_clause;
         subst.visit_with(visitor)
-            && delayed_literals.visit_with(visitor)
-            && constraints.visit_with(visitor)
-            && subgoals.visit_with(visitor)
+            || delayed_literals.visit_with(visitor)
+            || constraints.visit_with(visitor)
+            || subgoals.visit_with(visitor)
     }
 }
 
@@ -574,3 +657,59 @@ impl<'tcx, 'gcx: 'tcx, T> Upcast<'tcx, 'gcx> for Canonical<'gcx, T>
         }
     }
 }
+
+crate fn provide(p: &mut Providers) {
+    *p = Providers {
+        evaluate_goal,
+        ..*p
+    };
+}
+
+crate fn evaluate_goal<'a, 'tcx>(
+    tcx: TyCtxt<'a, 'tcx, 'tcx>,
+    goal: ChalkCanonicalGoal<'tcx>
+) -> Result<
+    Lrc<Canonical<'tcx, QueryResponse<'tcx, ()>>>,
+    traits::query::NoSolution
+> {
+    use crate::lowering::Lower;
+    use rustc::traits::WellFormed;
+
+    let goal = goal.unchecked_map(|goal| InEnvironment {
+        environment: goal.environment,
+        goal: match goal.goal {
+            ty::Predicate::WellFormed(ty) => tcx.mk_goal(
+                GoalKind::DomainGoal(DomainGoal::WellFormed(WellFormed::Ty(ty)))
+            ),
+
+            ty::Predicate::Subtype(predicate) => tcx.mk_goal(
+                GoalKind::Quantified(
+                    QuantifierKind::Universal,
+                    predicate.map_bound(|pred| tcx.mk_goal(GoalKind::Subtype(pred.a, pred.b)))
+                )
+            ),
+
+            other => tcx.mk_goal(
+                GoalKind::from_poly_domain_goal(other.lower(), tcx)
+            ),
+        },
+    });
+
+
+    debug!("evaluate_goal(goal = {:?})", goal);
+
+    let context = ChalkContext {
+        _arenas: ChalkArenas {
+            _phantom: PhantomData,
+        },
+        tcx,
+    };
+
+    let mut forest = Forest::new(context);
+    let solution = forest.solve(&goal);
+
+    debug!("evaluate_goal: solution = {:?}", solution);
+
+    solution.map(|ok| Ok(Lrc::new(ok)))
+        .unwrap_or(Err(traits::query::NoSolution))
+}

src/librustc_traits/chalk_context/program_clauses.rs

@@ -10,11 +10,13 @@ use rustc::traits::{
     Environment,
 };
 use rustc::ty;
+use rustc::ty::subst::{Substs, Subst};
 use rustc::hir;
 use rustc::hir::def_id::DefId;
 use rustc_target::spec::abi;
 use super::ChalkInferenceContext;
 use crate::lowering::Lower;
+use crate::generic_types;
 use std::iter;
 
 fn assemble_clauses_from_impls<'tcx>(
@@ -47,50 +49,152 @@ fn assemble_clauses_from_assoc_ty_values<'tcx>(
     });
 }
 
-fn program_clauses_for_raw_ptr<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
-    let ty = ty::Bound(
-        ty::INNERMOST,
-        ty::BoundVar::from_u32(0).into()
-    );
-    let ty = tcx.mk_ty(ty);
+fn assemble_builtin_sized_impls<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    sized_def_id: DefId,
+    ty: ty::Ty<'tcx>,
+    clauses: &mut Vec<Clause<'tcx>>
+) {
+    let mut push_builtin_impl = |ty: ty::Ty<'tcx>, nested: &[ty::Ty<'tcx>]| {
+        let clause = ProgramClause {
+            goal: ty::TraitPredicate {
+                trait_ref: ty::TraitRef {
+                    def_id: sized_def_id,
+                    substs: tcx.mk_substs_trait(ty, &[]),
+                },
+            }.lower(),
+            hypotheses: tcx.mk_goals(
+                nested.iter()
+                    .cloned()
+                    .map(|nested_ty| ty::TraitRef {
+                        def_id: sized_def_id,
+                        substs: tcx.mk_substs_trait(nested_ty, &[]),
+                    })
+                    .map(|trait_ref| ty::TraitPredicate { trait_ref })
+                    .map(|pred| GoalKind::DomainGoal(pred.lower()))
+                    .map(|goal_kind| tcx.mk_goal(goal_kind))
+            ),
+            category: ProgramClauseCategory::Other,
+        };
+        // Bind innermost bound vars that may exist in `ty` and `nested`.
+        clauses.push(Clause::ForAll(ty::Binder::bind(clause)));
+    };
 
-    let ptr_ty = tcx.mk_ptr(ty::TypeAndMut {
-        ty,
-        mutbl: hir::Mutability::MutImmutable,
-    });
+    match &ty.sty {
+        // Non parametric primitive types.
+        ty::Bool |
+        ty::Char |
+        ty::Int(..) |
+        ty::Uint(..) |
+        ty::Float(..) |
+        ty::Error |
+        ty::Never => push_builtin_impl(ty, &[]),
+
+        // These ones are always `Sized`.
+        &ty::Array(_, length) => {
+            push_builtin_impl(tcx.mk_ty(ty::Array(generic_types::bound(tcx, 0), length)), &[]);
+        }
+        ty::RawPtr(ptr) => {
+            push_builtin_impl(generic_types::raw_ptr(tcx, ptr.mutbl), &[]);
+        }
+        &ty::Ref(_, _, mutbl) => {
+            push_builtin_impl(generic_types::ref_ty(tcx, mutbl), &[]);
+        }
+        ty::FnPtr(fn_ptr) => {
+            let fn_ptr = fn_ptr.skip_binder();
+            let fn_ptr = generic_types::fn_ptr(
+                tcx,
+                fn_ptr.inputs_and_output.len(),
+                fn_ptr.variadic,
+                fn_ptr.unsafety,
+                fn_ptr.abi
+            );
+            push_builtin_impl(fn_ptr, &[]);
+        }
+        &ty::FnDef(def_id, ..) => {
+            push_builtin_impl(generic_types::fn_def(tcx, def_id), &[]);
+        }
+        &ty::Closure(def_id, ..) => {
+            push_builtin_impl(generic_types::closure(tcx, def_id), &[]);
+        }
+        &ty::Generator(def_id, ..) => {
+            push_builtin_impl(generic_types::generator(tcx, def_id), &[]);
+        }
+
+        // `Sized` if the last type is `Sized` (because else we will get a WF error anyway).
+        &ty::Tuple(type_list) => {
+            let type_list = generic_types::type_list(tcx, type_list.len());
+            push_builtin_impl(tcx.mk_ty(ty::Tuple(type_list)), &**type_list);
+        }
+
+        // Struct def
+        ty::Adt(adt_def, _) => {
+            let substs = Substs::bound_vars_for_item(tcx, adt_def.did);
+            let adt = tcx.mk_ty(ty::Adt(adt_def, substs));
+            let sized_constraint = adt_def.sized_constraint(tcx)
+                .iter()
+                .map(|ty| ty.subst(tcx, substs))
+                .collect::<Vec<_>>();
+            push_builtin_impl(adt, &sized_constraint);
+        }
+
+        // Artificially trigger an ambiguity.
+        ty::Infer(..) => {
+            // Everybody can find at least two types to unify against:
+            // general ty vars, int vars and float vars.
+            push_builtin_impl(tcx.types.i32, &[]);
+            push_builtin_impl(tcx.types.u32, &[]);
+            push_builtin_impl(tcx.types.f32, &[]);
+            push_builtin_impl(tcx.types.f64, &[]);
+        }
+
+        ty::Projection(_projection_ty) => {
+            // FIXME: add builtin impls from the associated type values found in
+            // trait impls of `projection_ty.trait_ref(tcx)`.
+        }
+
+        // The `Sized` bound can only come from the environment.
+        ty::Param(..) |
+        ty::Placeholder(..) |
+        ty::UnnormalizedProjection(..) => (),
+
+        // Definitely not `Sized`.
+        ty::Foreign(..) |
+        ty::Str |
+        ty::Slice(..) |
+        ty::Dynamic(..) |
+        ty::Opaque(..) => (),
+
+        ty::Bound(..) |
+        ty::GeneratorWitness(..) => bug!("unexpected type {:?}", ty),
+    }
+}
+
+fn wf_clause_for_raw_ptr<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    mutbl: hir::Mutability
+) -> Clauses<'tcx> {
+    let ptr_ty = generic_types::raw_ptr(tcx, mutbl);
 
     let wf_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(ptr_ty)),
         hypotheses: ty::List::empty(),
         category: ProgramClauseCategory::WellFormed,
     };
-    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+    let wf_clause = Clause::Implies(wf_clause);
 
     // `forall<T> { WellFormed(*const T). }`
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
-fn program_clauses_for_fn_ptr<'tcx>(
+fn wf_clause_for_fn_ptr<'tcx>(
     tcx: ty::TyCtxt<'_, '_, 'tcx>,
     arity_and_output: usize,
     variadic: bool,
     unsafety: hir::Unsafety,
     abi: abi::Abi
 ) -> Clauses<'tcx> {
-    let inputs_and_output = tcx.mk_type_list(
-        (0..arity_and_output).into_iter()
-            .map(|i| ty::BoundVar::from(i))
-            // DebruijnIndex(1) because we are going to inject these in a `PolyFnSig`
-            .map(|var| tcx.mk_ty(ty::Bound(ty::DebruijnIndex::from(1usize), var.into())))
-    );
-
-    let fn_sig = ty::Binder::bind(ty::FnSig {
-        inputs_and_output,
-        variadic,
-        unsafety,
-        abi,
-    });
-    let fn_ptr = tcx.mk_fn_ptr(fn_sig);
+    let fn_ptr = generic_types::fn_ptr(tcx, arity_and_output, variadic, unsafety, abi);
 
     let wf_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(fn_ptr)),
@@ -104,13 +208,8 @@ fn program_clauses_for_fn_ptr<'tcx>(
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
-fn program_clauses_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
-    let ty = ty::Bound(
-        ty::INNERMOST,
-        ty::BoundVar::from_u32(0).into()
-    );
-    let ty = tcx.mk_ty(ty);
-
+fn wf_clause_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+    let ty = generic_types::bound(tcx, 0);
     let slice_ty = tcx.mk_slice(ty);
 
     let sized_trait = match tcx.lang_items().sized_trait() {
@@ -138,16 +237,11 @@ fn program_clauses_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tc
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
-fn program_clauses_for_array<'tcx>(
+fn wf_clause_for_array<'tcx>(
     tcx: ty::TyCtxt<'_, '_, 'tcx>,
     length: &'tcx ty::Const<'tcx>
 ) -> Clauses<'tcx> {
-    let ty = ty::Bound(
-        ty::INNERMOST,
-        ty::BoundVar::from_u32(0).into()
-    );
-    let ty = tcx.mk_ty(ty);
-
+    let ty = generic_types::bound(tcx, 0);
     let array_ty = tcx.mk_ty(ty::Array(ty, length));
 
     let sized_trait = match tcx.lang_items().sized_trait() {
@@ -175,23 +269,21 @@ fn program_clauses_for_array<'tcx>(
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
-fn program_clauses_for_tuple<'tcx>(
+fn wf_clause_for_tuple<'tcx>(
     tcx: ty::TyCtxt<'_, '_, 'tcx>,
     arity: usize
 ) -> Clauses<'tcx> {
-    let type_list = tcx.mk_type_list(
-        (0..arity).into_iter()
-            .map(|i| ty::BoundVar::from(i))
-            .map(|var| tcx.mk_ty(ty::Bound(ty::INNERMOST, var.into())))
-    );
-
+    let type_list = generic_types::type_list(tcx, arity);
     let tuple_ty = tcx.mk_ty(ty::Tuple(type_list));
 
     let sized_trait = match tcx.lang_items().sized_trait() {
         Some(def_id) => def_id,
         None => return ty::List::empty(),
     };
-    let sized_implemented = type_list[0..arity - 1].iter()
+
+    // If `arity == 0` (i.e. the unit type) or `arity == 1`, this list of
+    // hypotheses is actually empty.
+    let sized_implemented = type_list[0 .. std::cmp::max(arity, 1) - 1].iter()
         .map(|ty| ty::TraitRef {
             def_id: sized_trait,
             substs: tcx.mk_substs_trait(*ty, ty::List::empty()),
@@ -221,26 +313,29 @@ fn program_clauses_for_tuple<'tcx>(
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
-fn program_clauses_for_ref<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+fn wf_clause_for_ref<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    mutbl: hir::Mutability
+) -> Clauses<'tcx> {
     let region = tcx.mk_region(
         ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
     );
-    let ty = tcx.mk_ty(
-        ty::Bound(ty::INNERMOST, ty::BoundVar::from_u32(1).into())
-    );
-
+    let ty = generic_types::bound(tcx, 1);
     let ref_ty = tcx.mk_ref(region, ty::TypeAndMut {
         ty,
-        mutbl: hir::Mutability::MutImmutable,
+        mutbl,
     });
 
-    let outlives: DomainGoal = ty::OutlivesPredicate(ty, region).lower();
+    let _outlives: DomainGoal = ty::OutlivesPredicate(ty, region).lower();
     let wf_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(ref_ty)),
-        hypotheses: tcx.mk_goals(
-            iter::once(tcx.mk_goal(outlives.into_goal()))
-        ),
-        category: ProgramClauseCategory::ImpliedBound,
+        hypotheses: ty::List::empty(),
+
+        // FIXME: restore this later once we get better at handling regions
+        // hypotheses: tcx.mk_goals(
+        //     iter::once(tcx.mk_goal(outlives.into_goal()))
+        // ),
+        category: ProgramClauseCategory::WellFormed,
     };
     let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
 
@@ -248,6 +343,24 @@ fn program_clauses_for_ref<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx>
     tcx.mk_clauses(iter::once(wf_clause))
 }
 
+fn wf_clause_for_fn_def<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    def_id: DefId
+) -> Clauses<'tcx> {
+    let fn_def = generic_types::fn_def(tcx, def_id);
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(fn_def)),
+        hypotheses: ty::List::empty(),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall <T1, ..., Tn+1> { WellFormed(fn some_fn(T1, ..., Tn) -> Tn+1). }`
+    // where `def_id` maps to the `some_fn` function definition
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
 impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
     pub(super) fn program_clauses_impl(
         &self,
@@ -255,6 +368,11 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
         goal: &DomainGoal<'tcx>,
     ) -> Vec<Clause<'tcx>> {
         use rustc::traits::WhereClause::*;
+        use rustc::infer::canonical::OriginalQueryValues;
+
+        let goal = self.infcx.resolve_type_vars_if_possible(goal);
+
+        debug!("program_clauses(goal = {:?})", goal);
 
         let mut clauses = match goal {
             DomainGoal::Holds(Implemented(trait_predicate)) => {
@@ -263,12 +381,22 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
                 // * the trait decl (rule `Implemented-From-Env`)
 
                 let mut clauses = vec![];
+
                 assemble_clauses_from_impls(
                     self.infcx.tcx,
                     trait_predicate.def_id(),
                     &mut clauses
                 );
 
+                if Some(trait_predicate.def_id()) == self.infcx.tcx.lang_items().sized_trait() {
+                    assemble_builtin_sized_impls(
+                        self.infcx.tcx,
+                        trait_predicate.def_id(),
+                        trait_predicate.self_ty(),
+                        &mut clauses
+                    );
+                }
+
                 // FIXME: we need to add special rules for builtin impls:
                 // * `Copy` / `Clone`
                 // * `Sized`
@@ -345,31 +473,34 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
                         self.infcx.tcx.program_clauses_for(data.item_def_id)
                     }
 
-                    // These types are always WF and non-parametric.
+                    // These types are always WF.
                     ty::Bool |
                     ty::Char |
                     ty::Int(..) |
                     ty::Uint(..) |
                     ty::Float(..) |
                     ty::Str |
+                    ty::Param(..) |
+                    ty::Placeholder(..) |
+                    ty::Error |
                     ty::Never => {
                         let wf_clause = ProgramClause {
                             goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
                             hypotheses: ty::List::empty(),
                             category: ProgramClauseCategory::WellFormed,
                         };
-                        let wf_clause = Clause::ForAll(ty::Binder::dummy(wf_clause));
+                        let wf_clause = Clause::Implies(wf_clause);
 
                         self.infcx.tcx.mk_clauses(iter::once(wf_clause))
                     }
 
                     // Always WF (recall that we do not check for parameters to be WF).
-                    ty::RawPtr(..) => program_clauses_for_raw_ptr(self.infcx.tcx),
+                    ty::RawPtr(ptr) => wf_clause_for_raw_ptr(self.infcx.tcx, ptr.mutbl),
 
                     // Always WF (recall that we do not check for parameters to be WF).
                     ty::FnPtr(fn_ptr) => {
                         let fn_ptr = fn_ptr.skip_binder();
-                        program_clauses_for_fn_ptr(
+                        wf_clause_for_fn_ptr(
                             self.infcx.tcx,
                             fn_ptr.inputs_and_output.len(),
                             fn_ptr.variadic,
@@ -379,19 +510,21 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
                     }
 
                     // WF if inner type is `Sized`.
-                    ty::Slice(..) => program_clauses_for_slice(self.infcx.tcx),
+                    ty::Slice(..) => wf_clause_for_slice(self.infcx.tcx),
 
                     // WF if inner type is `Sized`.
-                    ty::Array(_, length) => program_clauses_for_array(self.infcx.tcx, length),
+                    ty::Array(_, length) => wf_clause_for_array(self.infcx.tcx, length),
 
                     // WF if all types but the last one are `Sized`.
-                    ty::Tuple(types) => program_clauses_for_tuple(
+                    ty::Tuple(types) => wf_clause_for_tuple(
                         self.infcx.tcx,
                         types.len()
                     ),
 
                     // WF if `sub_ty` outlives `region`.
-                    ty::Ref(..) => program_clauses_for_ref(self.infcx.tcx),
+                    ty::Ref(_, _, mutbl) => wf_clause_for_ref(self.infcx.tcx, mutbl),
+
+                    ty::FnDef(def_id, ..) => wf_clause_for_fn_def(self.infcx.tcx, def_id),
 
                     ty::Dynamic(..) => {
                         // FIXME: no rules yet for trait objects
@@ -402,21 +535,32 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
                         self.infcx.tcx.program_clauses_for(def.did)
                     }
 
+                    // FIXME: these are probably wrong
                     ty::Foreign(def_id) |
-                    ty::FnDef(def_id, ..) |
                     ty::Closure(def_id, ..) |
                     ty::Generator(def_id, ..) |
                     ty::Opaque(def_id, ..) => {
                         self.infcx.tcx.program_clauses_for(def_id)
                     }
 
+                    // Artificially trigger an ambiguity.
+                    ty::Infer(..) => {
+                        let tcx = self.infcx.tcx;
+                        let types = [tcx.types.i32, tcx.types.u32, tcx.types.f32, tcx.types.f64];
+                        let clauses = types.iter()
+                            .cloned()
+                            .map(|ty| ProgramClause {
+                                goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
+                                hypotheses: ty::List::empty(),
+                                category: ProgramClauseCategory::WellFormed,
+                            })
+                            .map(|clause| Clause::Implies(clause));
+                        tcx.mk_clauses(clauses)
+                    }
+
                     ty::GeneratorWitness(..) |
-                    ty::Placeholder(..) |
                     ty::UnnormalizedProjection(..) |
-                    ty::Infer(..) |
-                    ty::Bound(..) |
-                    ty::Param(..) |
-                    ty::Error => {
+                    ty::Bound(..) => {
                         bug!("unexpected type {:?}", ty)
                     }
                 };
@@ -458,13 +602,20 @@ impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
             }
         };
 
-        let environment = self.infcx.tcx.lift_to_global(environment)
-            .expect("environment is not global");
-        clauses.extend(
-            self.infcx.tcx.program_clauses_for_env(environment)
-                .into_iter()
-                .cloned()
-        );
+        debug!("program_clauses: clauses = {:?}", clauses);
+        debug!("program_clauses: adding clauses from environment = {:?}", environment);
+
+        let mut _orig_query_values = OriginalQueryValues::default();
+        let canonical_environment = self.infcx.canonicalize_query(
+            environment,
+            &mut _orig_query_values
+        ).value;
+        let env_clauses = self.infcx.tcx.program_clauses_for_env(canonical_environment);
+
+        debug!("program_clauses: env_clauses = {:?}", env_clauses);
+
+        clauses.extend(env_clauses.into_iter().cloned());
+        clauses.extend(environment.clauses.iter().cloned());
         clauses
     }
 }

src/librustc_traits/chalk_context/resolvent_ops.rs

@@ -35,7 +35,9 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     ) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
         use chalk_engine::context::UnificationOps;
 
-        self.infcx.probe(|_| {
+        debug!("resolvent_clause(goal = {:?}, clause = {:?})", goal, clause);
+
+        let result = self.infcx.probe(|_| {
             let ProgramClause {
                 goal: consequence,
                 hypotheses,
@@ -49,8 +51,13 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
                 ).0,
             };
 
-            let result = unify(self.infcx, *environment, goal, &consequence)
-                .map_err(|_| NoSolution)?;
+            let result = unify(
+                self.infcx,
+                *environment,
+                ty::Variance::Invariant,
+                goal,
+                &consequence
+            ).map_err(|_| NoSolution)?;
 
             let mut ex_clause = ExClause {
                 subst: subst.clone(),
@@ -70,7 +77,10 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 
             let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
             Ok(canonical_ex_clause)
-        })
+        });
+
+        debug!("resolvent_clause: result = {:?}", result);
+        result
     }
 
     fn apply_answer_subst(
@@ -80,6 +90,12 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
         canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
     ) -> Fallible<ChalkExClause<'tcx>> {
+        debug!(
+            "apply_answer_subst(ex_clause = {:?}, selected_goal = {:?})",
+            self.infcx.resolve_type_vars_if_possible(&ex_clause),
+            self.infcx.resolve_type_vars_if_possible(selected_goal)
+        );
+
         let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
             DUMMY_SP,
             canonical_answer_subst
@@ -96,8 +112,12 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         substitutor.relate(&answer_table_goal.value, &selected_goal)
             .map_err(|_| NoSolution)?;
 
-        let mut ex_clause = substitutor.ex_clause;
-        ex_clause.constraints.extend(answer_subst.constraints);
+        let ex_clause = substitutor.ex_clause;
+
+        // FIXME: restore this later once we get better at handling regions
+        // ex_clause.constraints.extend(answer_subst.constraints);
+
+        debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
         Ok(ex_clause)
     }
 }
@@ -124,7 +144,7 @@ impl AnswerSubstitutor<'cx, 'gcx, 'tcx> {
         );
 
         super::into_ex_clause(
-            unify(self.infcx, self.environment, answer_param, pending)?,
+            unify(self.infcx, self.environment, ty::Variance::Invariant, answer_param, pending)?,
             &mut self.ex_clause
         );
 
@@ -172,6 +192,7 @@ impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
 
     fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
         let b = self.infcx.shallow_resolve(b);
+        debug!("AnswerSubstitutor::tys(a = {:?}, b = {:?})", a, b);
 
         if let &ty::Bound(debruijn, bound_ty) = &a.sty {
             // Free bound var

src/librustc_traits/chalk_context/unify.rs

@@ -13,9 +13,16 @@ crate struct UnificationResult<'tcx> {
 crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
     infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
     environment: Environment<'tcx>,
+    variance: ty::Variance,
     a: &T,
     b: &T
 ) -> RelateResult<'tcx, UnificationResult<'tcx>> {
+    debug!("unify(
+        a = {:?},
+        b = {:?},
+        environment = {:?},
+    )", a, b, environment);
+
     let mut delegate = ChalkTypeRelatingDelegate::new(
         infcx,
         environment
@@ -24,9 +31,11 @@ crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
     TypeRelating::new(
         infcx,
         &mut delegate,
-        ty::Variance::Invariant
+        variance
     ).relate(a, b)?;
 
+    debug!("unify: goals = {:?}, constraints = {:?}", delegate.goals, delegate.constraints);
+
     Ok(UnificationResult {
         goals: delegate.goals,
         constraints: delegate.constraints,

src/librustc_traits/dropck_outlives.rs

@@ -2,7 +2,7 @@ use rustc::hir::def_id::DefId;
 use rustc::infer::canonical::{Canonical, QueryResponse};
 use rustc::traits::query::dropck_outlives::{DropckOutlivesResult, DtorckConstraint};
 use rustc::traits::query::{CanonicalTyGoal, NoSolution};
-use rustc::traits::{FulfillmentContext, Normalized, ObligationCause, TraitEngineExt};
+use rustc::traits::{TraitEngine, Normalized, ObligationCause, TraitEngineExt};
 use rustc::ty::query::Providers;
 use rustc::ty::subst::{Subst, Substs};
 use rustc::ty::{self, ParamEnvAnd, Ty, TyCtxt};
@@ -78,7 +78,7 @@ fn dropck_outlives<'tcx>(
             // Set used to detect infinite recursion.
             let mut ty_set = FxHashSet::default();
 
-            let fulfill_cx = &mut FulfillmentContext::new();
+            let mut fulfill_cx = TraitEngine::new(infcx.tcx);
 
             let cause = ObligationCause::dummy();
             while let Some((ty, depth)) = ty_stack.pop() {
@@ -136,7 +136,11 @@ fn dropck_outlives<'tcx>(
 
             debug!("dropck_outlives: result = {:#?}", result);
 
-            infcx.make_canonicalized_query_response(canonical_inference_vars, result, fulfill_cx)
+            infcx.make_canonicalized_query_response(
+                canonical_inference_vars,
+                result,
+                &mut *fulfill_cx
+            )
         },
     )
 }

src/librustc_traits/generic_types.rs

@@ -0,0 +1,80 @@
+//! Utilities for creating generic types with bound vars in place of parameter values.
+
+use rustc::ty::{self, Ty, TyCtxt};
+use rustc::ty::subst::Substs;
+use rustc::hir;
+use rustc::hir::def_id::DefId;
+use rustc_target::spec::abi;
+
+crate fn bound(tcx: ty::TyCtxt<'_, '_, 'tcx>, index: u32) -> Ty<'tcx> {
+    let ty = ty::Bound(
+        ty::INNERMOST,
+        ty::BoundVar::from_u32(index).into()
+    );
+    tcx.mk_ty(ty)
+}
+
+crate fn raw_ptr(tcx: TyCtxt<'_, '_, 'tcx>, mutbl: hir::Mutability) -> Ty<'tcx> {
+    tcx.mk_ptr(ty::TypeAndMut {
+        ty: bound(tcx, 0),
+        mutbl,
+    })
+}
+
+crate fn fn_ptr(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    arity_and_output: usize,
+    variadic: bool,
+    unsafety: hir::Unsafety,
+    abi: abi::Abi
+) -> Ty<'tcx> {
+    let inputs_and_output = tcx.mk_type_list(
+        (0..arity_and_output).into_iter()
+            .map(|i| ty::BoundVar::from(i))
+            // DebruijnIndex(1) because we are going to inject these in a `PolyFnSig`
+            .map(|var| tcx.mk_ty(ty::Bound(ty::DebruijnIndex::from(1usize), var.into())))
+    );
+
+    let fn_sig = ty::Binder::bind(ty::FnSig {
+        inputs_and_output,
+        variadic,
+        unsafety,
+        abi,
+    });
+    tcx.mk_fn_ptr(fn_sig)
+}
+
+crate fn type_list(tcx: ty::TyCtxt<'_, '_, 'tcx>, arity: usize) -> &'tcx ty::List<Ty<'tcx>> {
+    tcx.mk_type_list(
+        (0..arity).into_iter()
+            .map(|i| ty::BoundVar::from(i))
+            .map(|var| tcx.mk_ty(ty::Bound(ty::INNERMOST, var.into())))
+    )
+}
+
+crate fn ref_ty(tcx: ty::TyCtxt<'_, '_, 'tcx>, mutbl: hir::Mutability) -> Ty<'tcx> {
+    let region = tcx.mk_region(
+        ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
+    );
+
+    tcx.mk_ref(region, ty::TypeAndMut {
+        ty: bound(tcx, 1),
+        mutbl,
+    })
+}
+
+crate fn fn_def(tcx: ty::TyCtxt<'_, '_, 'tcx>, def_id: DefId) -> Ty<'tcx> {
+    tcx.mk_ty(ty::FnDef(def_id, Substs::bound_vars_for_item(tcx, def_id)))
+}
+
+crate fn closure(tcx: ty::TyCtxt<'_, '_, 'tcx>, def_id: DefId) -> Ty<'tcx> {
+    tcx.mk_closure(def_id, ty::ClosureSubsts {
+        substs: Substs::bound_vars_for_item(tcx, def_id),
+    })
+}
+
+crate fn generator(tcx: ty::TyCtxt<'_, '_, 'tcx>, def_id: DefId) -> Ty<'tcx> {
+    tcx.mk_generator(def_id, ty::GeneratorSubsts {
+        substs: Substs::bound_vars_for_item(tcx, def_id),
+    }, hir::GeneratorMovability::Movable)
+}

src/librustc_traits/lib.rs

@@ -25,6 +25,7 @@ mod implied_outlives_bounds;
 mod normalize_projection_ty;
 mod normalize_erasing_regions;
 pub mod lowering;
+mod generic_types;
 mod type_op;
 
 use rustc::ty::query::Providers;
@@ -34,6 +35,7 @@ pub fn provide(p: &mut Providers) {
     evaluate_obligation::provide(p);
     implied_outlives_bounds::provide(p);
     lowering::provide(p);
+    chalk_context::provide(p);
     normalize_projection_ty::provide(p);
     normalize_erasing_regions::provide(p);
     type_op::provide(p);

src/librustc_traits/lowering/environment.rs

@@ -11,6 +11,7 @@ use rustc::ty::{self, TyCtxt, Ty};
 use rustc::hir::def_id::DefId;
 use rustc_data_structures::fx::FxHashSet;
 use super::Lower;
+use crate::generic_types;
 use std::iter;
 
 struct ClauseVisitor<'set, 'a, 'tcx: 'a + 'set> {
@@ -38,20 +39,16 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
             }
 
             // forall<'a, T> { `Outlives(T: 'a) :- FromEnv(&'a T)` }
-            ty::Ref(..) => {
-                use rustc::hir;
-
+            ty::Ref(_, _, mutbl) => {
                 let region = self.tcx.mk_region(
                     ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
                 );
-                let ty = self.tcx.mk_ty(
-                    ty::Bound(ty::INNERMOST, ty::BoundVar::from_u32(1).into())
-                );
-
+                let ty = generic_types::bound(self.tcx, 1);
                 let ref_ty = self.tcx.mk_ref(region, ty::TypeAndMut {
                     ty,
-                    mutbl: hir::Mutability::MutImmutable,
+                    mutbl,
                 });
+
                 let from_env = DomainGoal::FromEnv(FromEnv::Ty(ref_ty));
 
                 let clause = ProgramClause {
@@ -105,11 +102,11 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
             ty::Never |
             ty::Infer(..) |
             ty::Placeholder(..) |
+            ty::Param(..) |
             ty::Bound(..) => (),
 
             ty::GeneratorWitness(..) |
             ty::UnnormalizedProjection(..) |
-            ty::Param(..) |
             ty::Error => {
                 bug!("unexpected type {:?}", ty);
             }
@@ -192,25 +189,23 @@ crate fn program_clauses_for_env<'a, 'tcx>(
 crate fn environment<'a, 'tcx>(
     tcx: TyCtxt<'a, 'tcx, 'tcx>,
     def_id: DefId
-) -> ty::Binder<Environment<'tcx>> {
+) -> Environment<'tcx> {
     use super::{Lower, IntoFromEnvGoal};
     use rustc::hir::{Node, TraitItemKind, ImplItemKind, ItemKind, ForeignItemKind};
-    use rustc::ty::subst::{Subst, Substs};
+
+    debug!("environment(def_id = {:?})", def_id);
 
     // The environment of an impl Trait type is its defining function's environment.
     if let Some(parent) = ty::is_impl_trait_defn(tcx, def_id) {
         return environment(tcx, parent);
     }
 
-    let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
-
     // Compute the bounds on `Self` and the type parameters.
     let ty::InstantiatedPredicates { predicates } = tcx.predicates_of(def_id)
         .instantiate_identity(tcx);
 
     let clauses = predicates.into_iter()
         .map(|predicate| predicate.lower())
-        .map(|predicate| predicate.subst(tcx, bound_vars))
         .map(|domain_goal| domain_goal.map_bound(|bound| bound.into_from_env_goal()))
         .map(|domain_goal| domain_goal.map_bound(|bound| bound.into_program_clause()))
 
@@ -221,73 +216,85 @@ crate fn environment<'a, 'tcx>(
     let node_id = tcx.hir().as_local_node_id(def_id).unwrap();
     let node = tcx.hir().get(node_id);
 
-    let mut is_fn = false;
-    let mut is_impl = false;
-    match node {
+    enum NodeKind {
+        TraitImpl,
+        InherentImpl,
+        Fn,
+        Other,
+    };
+
+    let node_kind = match node {
         Node::TraitItem(item) => match item.node {
-            TraitItemKind::Method(..) => is_fn = true,
-            _ => (),
+            TraitItemKind::Method(..) => NodeKind::Fn,
+            _ => NodeKind::Other,
         }
 
         Node::ImplItem(item) => match item.node {
-            ImplItemKind::Method(..) => is_fn = true,
-            _ => (),
+            ImplItemKind::Method(..) => NodeKind::Fn,
+            _ => NodeKind::Other,
         }
 
         Node::Item(item) => match item.node {
-            ItemKind::Impl(..) => is_impl = true,
-            ItemKind::Fn(..) => is_fn = true,
-            _ => (),
+            ItemKind::Impl(.., Some(..), _, _) => NodeKind::TraitImpl,
+            ItemKind::Impl(.., None, _, _) => NodeKind::InherentImpl,
+            ItemKind::Fn(..) => NodeKind::Fn,
+            _ => NodeKind::Other,
         }
 
         Node::ForeignItem(item) => match item.node {
-            ForeignItemKind::Fn(..) => is_fn = true,
-            _ => (),
+            ForeignItemKind::Fn(..) => NodeKind::Fn,
+            _ => NodeKind::Other,
         }
 
         // FIXME: closures?
-        _ => (),
-    }
+        _ => NodeKind::Other,
+    };
 
     let mut input_tys = FxHashSet::default();
 
-    // In an impl, we assume that the header trait ref and all its constituents
-    // are well-formed.
-    if is_impl {
-        let trait_ref = tcx.impl_trait_ref(def_id)
-            .expect("not an impl")
-            .subst(tcx, bound_vars);
+    match node_kind {
+        // In a trait impl, we assume that the header trait ref and all its
+        // constituents are well-formed.
+        NodeKind::TraitImpl => {
+            let trait_ref = tcx.impl_trait_ref(def_id)
+                .expect("not an impl");
 
-        input_tys.extend(
-            trait_ref.substs.types().flat_map(|ty| ty.walk())
-        );
-    }
+            input_tys.extend(
+                trait_ref.input_types().flat_map(|ty| ty.walk())
+            );
+        }
 
-    // In an fn, we assume that the arguments and all their constituents are
-    // well-formed.
-    if is_fn {
-        // `skip_binder` because we move region parameters to the root binder,
-        // restored in the return type of this query
-        let fn_sig = tcx.fn_sig(def_id).skip_binder().subst(tcx, bound_vars);
+        // In an inherent impl, we assume that the receiver type and all its
+        // constituents are well-formed.
+        NodeKind::InherentImpl => {
+            let self_ty = tcx.type_of(def_id);
+            input_tys.extend(self_ty.walk());
+        }
 
-        input_tys.extend(
-            fn_sig.inputs().iter().flat_map(|ty| ty.walk())
-        );
+        // In an fn, we assume that the arguments and all their constituents are
+        // well-formed.
+        NodeKind::Fn => {
+            let fn_sig = tcx.fn_sig(def_id);
+            let fn_sig = tcx.liberate_late_bound_regions(def_id, &fn_sig);
+
+            input_tys.extend(
+                fn_sig.inputs().iter().flat_map(|ty| ty.walk())
+            );
+        }
+
+        NodeKind::Other => (),
     }
 
     let clauses = clauses.chain(
         input_tys.into_iter()
-            // Filter out type parameters
-            .filter(|ty| match ty.sty {
-                ty::Bound(..) => false,
-                _ => true,
-            })
             .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty)))
             .map(|domain_goal| domain_goal.into_program_clause())
             .map(Clause::Implies)
     );
 
-    ty::Binder::bind(Environment {
+    debug!("environment: clauses = {:?}", clauses);
+
+    Environment {
         clauses: tcx.mk_clauses(clauses),
-    })
+    }
 }

src/librustc_traits/lowering/mod.rs

@@ -211,7 +211,6 @@ fn program_clauses_for_trait<'a, 'tcx>(
     let where_clauses = &predicates
         .iter()
         .map(|(wc, _)| wc.lower())
-        .map(|wc| wc.subst(tcx, bound_vars))
         .collect::<Vec<_>>();
 
     // Rule Implied-Bound-From-Trait
@@ -232,14 +231,13 @@ fn program_clauses_for_trait<'a, 'tcx>(
         .map(|wc| {
             // we move binders to the left
             wc.map_bound(|goal| ProgramClause {
-                goal: goal.into_from_env_goal(),
-
-                // FIXME: As where clauses can only bind lifetimes for now,
-                // and that named bound regions have a def-id, it is safe
-                // to just inject `hypotheses` (which contains named vars bound at index `0`)
-                // into this binding level. This may change if we ever allow where clauses
-                // to bind types (e.g., for GATs things), because bound types only use a `BoundVar`
+                // FIXME: As where clauses can only bind lifetimes for now, and that named
+                // bound regions have a def-id, it is safe to just inject `bound_vars` and
+                // `hypotheses` (which contain named vars bound at index `0`) into this
+                // binding level. This may change if we ever allow where clauses to bind
+                // types (e.g. for GATs things), because bound types only use a `BoundVar`
                 // index (no def-id).
+                goal: goal.subst(tcx, bound_vars).into_from_env_goal(),
                 hypotheses,
 
                 category: ProgramClauseCategory::ImpliedBound,
@@ -346,7 +344,6 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
     let where_clauses = tcx.predicates_of(def_id).predicates
         .iter()
         .map(|(wc, _)| wc.lower())
-        .map(|wc| wc.subst(tcx, bound_vars))
         .collect::<Vec<_>>();
 
     // `WellFormed(Ty<...>) :- WC1, ..., WCm`
@@ -355,7 +352,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
         hypotheses: tcx.mk_goals(
             where_clauses
                 .iter()
-                .cloned()
+                .map(|wc| wc.subst(tcx, bound_vars))
                 .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
         ),
         category: ProgramClauseCategory::WellFormed,
@@ -383,11 +380,10 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
         .map(|wc| {
             // move the binders to the left
             wc.map_bound(|goal| ProgramClause {
-                goal: goal.into_from_env_goal(),
-
-                // FIXME: we inject `hypotheses` into this binding level,
-                // which may be incorrect in the future: see the FIXME in
-                // `program_clauses_for_trait`
+                // FIXME: we inject `bound_vars` and `hypotheses` into this binding
+                // level, which may be incorrect in the future: see the FIXME in
+                // `program_clauses_for_trait`.
+                goal: goal.subst(tcx, bound_vars).into_from_env_goal(),
                 hypotheses,
 
                 category: ProgramClauseCategory::ImpliedBound,
@@ -626,7 +622,7 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
 
             if attr.check_name("rustc_dump_env_program_clauses") {
                 let environment = self.tcx.environment(def_id);
-                clauses = Some(self.tcx.program_clauses_for_env(*environment.skip_binder()));
+                clauses = Some(self.tcx.program_clauses_for_env(environment));
             }
 
             if let Some(clauses) = clauses {

src/librustc_traits/type_op.rs

@@ -11,7 +11,7 @@ use rustc::traits::query::type_op::prove_predicate::ProvePredicate;
 use rustc::traits::query::type_op::subtype::Subtype;
 use rustc::traits::query::{Fallible, NoSolution};
 use rustc::traits::{
-    FulfillmentContext, Normalized, Obligation, ObligationCause, TraitEngine, TraitEngineExt,
+    Normalized, Obligation, ObligationCause, TraitEngine, TraitEngineExt,
 };
 use rustc::ty::query::Providers;
 use rustc::ty::subst::{Kind, Subst, UserSelfTy, UserSubsts};
@@ -75,7 +75,7 @@ fn type_op_ascribe_user_type<'tcx>(
 struct AscribeUserTypeCx<'me, 'gcx: 'tcx, 'tcx: 'me> {
     infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
     param_env: ParamEnv<'tcx>,
-    fulfill_cx: &'me mut FulfillmentContext<'tcx>,
+    fulfill_cx: &'me mut dyn TraitEngine<'tcx>,
 }
 
 impl AscribeUserTypeCx<'me, 'gcx, 'tcx> {
@@ -231,7 +231,7 @@ fn type_op_eq<'tcx>(
 
 fn type_op_normalize<T>(
     infcx: &InferCtxt<'_, 'gcx, 'tcx>,
-    fulfill_cx: &mut FulfillmentContext<'tcx>,
+    fulfill_cx: &mut dyn TraitEngine<'tcx>,
     key: ParamEnvAnd<'tcx, Normalize<T>>,
 ) -> Fallible<T>
 where

src/librustc_typeck/check/compare_method.rs

@@ -206,8 +206,11 @@ fn compare_predicate_entailment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     // The key step here is to update the caller_bounds's predicates to be
     // the new hybrid bounds we computed.
     let normalize_cause = traits::ObligationCause::misc(impl_m_span, impl_m_node_id);
-    let param_env = ty::ParamEnv::new(tcx.intern_predicates(&hybrid_preds.predicates),
-                                      Reveal::UserFacing);
+    let param_env = ty::ParamEnv::new(
+        tcx.intern_predicates(&hybrid_preds.predicates),
+        Reveal::UserFacing,
+        None
+    );
     let param_env = traits::normalize_param_env_or_error(tcx,
                                                          impl_m.def_id,
                                                          param_env,

src/test/compile-fail/chalkify/chalk_initial_program.rs

@@ -0,0 +1,16 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+
+impl Foo for i32 { }
+
+impl Foo for u32 { }
+
+fn gimme<F: Foo>() { }
+
+// Note: this also tests that `std::process::Termination` is implemented for `()`.
+fn main() {
+    gimme::<i32>();
+    gimme::<u32>();
+    gimme::<f32>(); //~ERROR the trait bound `f32: Foo` is not satisfied
+}

src/test/compile-fail/chalkify/generic_impls.rs

@@ -0,0 +1,18 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+
+impl<T> Foo for (T, u32) { }
+
+fn gimme<F: Foo>() { }
+
+fn foo<T>() {
+    gimme::<(T, u32)>();
+    gimme::<(Option<T>, u32)>();
+    gimme::<(Option<T>, f32)>(); //~ ERROR
+}
+
+fn main() {
+    gimme::<(i32, u32)>();
+    gimme::<(i32, f32)>(); //~ ERROR
+}

src/test/compile-fail/chalkify/impl_wf.rs

@@ -0,0 +1,38 @@
+// compile-flags: -Z chalk
+
+trait Foo: Sized { }
+
+trait Bar {
+    type Item: Foo;
+}
+
+impl Foo for i32 { }
+
+impl Foo for str { }
+//~^ ERROR the size for values of type `str` cannot be known at compilation time
+
+// Implicit `T: Sized` bound.
+impl<T> Foo for Option<T> { }
+
+impl Bar for () {
+    type Item = i32;
+}
+
+impl<T> Bar for Option<T> {
+    type Item = Option<T>;
+}
+
+impl Bar for f32 {
+//~^ ERROR the trait bound `f32: Foo` is not satisfied
+    type Item = f32;
+}
+
+trait Baz<U: ?Sized> where U: Foo { }
+
+impl Baz<i32> for i32 { }
+
+impl Baz<f32> for f32 { }
+//~^ ERROR the trait bound `f32: Foo` is not satisfied
+
+fn main() {
+}

src/test/compile-fail/chalkify/type_wf.rs

@@ -0,0 +1,24 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+
+struct S<T: Foo> {
+    x: T,
+}
+
+impl Foo for i32 { }
+impl<T> Foo for Option<T> { }
+
+fn main() {
+    let s = S {
+       x: 5,
+    };
+
+    let s = S { //~ ERROR the trait bound `{float}: Foo` is not satisfied
+        x: 5.0,
+    };
+
+    let s = S {
+        x: Some(5.0),
+    };
+}

src/test/run-pass/chalkify/inherent_impl.rs

@@ -0,0 +1,41 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+
+impl Foo for i32 { }
+
+struct S<T: Foo> {
+    x: T,
+}
+
+fn only_foo<T: Foo>(_x: &T) { }
+
+impl<T> S<T> {
+    // Test that we have the correct environment inside an inherent method.
+    fn dummy_foo(&self) {
+        only_foo(&self.x)
+    }
+}
+
+trait Bar { }
+impl Bar for u32 { }
+
+fn only_bar<T: Bar>() { }
+
+impl<T> S<T> {
+    // Test that the environment of `dummy_bar` adds up with the environment
+    // of the inherent impl.
+    fn dummy_bar<U: Bar>(&self) {
+        only_foo(&self.x);
+        only_bar::<U>();
+    }
+}
+
+fn main() {
+    let s = S {
+        x: 5,
+    };
+
+    s.dummy_foo();
+    s.dummy_bar::<u32>();
+}

src/test/run-pass/chalkify/projection.rs

@@ -0,0 +1,24 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+
+trait Bar {
+    type Item: Foo;
+}
+
+impl Foo for i32 { }
+impl Bar for i32 {
+    type Item = i32;
+}
+
+fn only_foo<T: Foo>() { }
+
+fn only_bar<T: Bar>() {
+    // `T` implements `Bar` hence `<T as Bar>::Item` must also implement `Bar`
+    only_foo::<T::Item>()
+}
+
+fn main() {
+    only_bar::<i32>();
+    only_foo::<<i32 as Bar>::Item>();
+}

src/test/run-pass/chalkify/super_trait.rs

@@ -0,0 +1,18 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+trait Bar: Foo { }
+
+impl Foo for i32 { }
+impl Bar for i32 { }
+
+fn only_foo<T: Foo>() { }
+
+fn only_bar<T: Bar>() {
+    // `T` implements `Bar` hence `T` must also implement `Foo`
+    only_foo::<T>()
+}
+
+fn main() {
+    only_bar::<i32>()
+}

src/test/run-pass/chalkify/trait_implied_bound.rs

@@ -0,0 +1,17 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+trait Bar<U> where U: Foo { }
+
+impl Foo for i32 { }
+impl Bar<i32> for i32 { }
+
+fn only_foo<T: Foo>() { }
+
+fn only_bar<U, T: Bar<U>>() {
+    only_foo::<U>()
+}
+
+fn main() {
+    only_bar::<i32, i32>()
+}

src/test/run-pass/chalkify/type_implied_bound.rs

@@ -0,0 +1,28 @@
+// compile-flags: -Z chalk
+
+trait Eq { }
+trait Hash: Eq { }
+
+impl Eq for i32 { }
+impl Hash for i32 { }
+
+struct Set<T: Hash> {
+    _x: T,
+}
+
+fn only_eq<T: Eq>() { }
+
+fn take_a_set<T>(_: &Set<T>) {
+    // `Set<T>` is an input type of `take_a_set`, hence we know that
+    // `T` must implement `Hash`, and we know in turn that `T` must
+    // implement `Eq`.
+    only_eq::<T>()
+}
+
+fn main() {
+    let set = Set {
+        _x: 5,
+    };
+
+    take_a_set(&set);
+}

src/test/ui/chalkify/type_inference.rs

@@ -0,0 +1,26 @@
+// compile-flags: -Z chalk
+
+trait Foo { }
+impl Foo for i32 { }
+
+trait Bar { }
+impl Bar for i32 { }
+impl Bar for u32 { }
+
+fn only_foo<T: Foo>(_x: T) { }
+
+fn only_bar<T: Bar>(_x: T) { }
+
+fn main() {
+    let x = 5.0;
+
+    // The only type which implements `Foo` is `i32`, so the chalk trait solver
+    // is expecting a variable of type `i32`. This behavior differs from the
+    // old-style trait solver. I guess this will change, that's why I'm
+    // adding that test.
+    only_foo(x); //~ ERROR mismatched types
+
+    // Here we have two solutions so we get back the behavior of the old-style
+    // trait solver.
+    only_bar(x); //~ ERROR the trait bound `{float}: Bar` is not satisfied
+}

src/test/ui/chalkify/type_inference.stderr

@@ -0,0 +1,28 @@
+error[E0308]: mismatched types
+  --> $DIR/type_inference.rs:21:14
+   |
+LL |     only_foo(x); //~ ERROR mismatched types
+   |              ^ expected i32, found floating-point variable
+   |
+   = note: expected type `i32`
+              found type `{float}`
+
+error[E0277]: the trait bound `{float}: Bar` is not satisfied
+  --> $DIR/type_inference.rs:25:5
+   |
+LL |     only_bar(x); //~ ERROR the trait bound `{float}: Bar` is not satisfied
+   |     ^^^^^^^^ the trait `Bar` is not implemented for `{float}`
+   |
+   = help: the following implementations were found:
+             <i32 as Bar>
+             <u32 as Bar>
+note: required by `only_bar`
+  --> $DIR/type_inference.rs:12:1
+   |
+LL | fn only_bar<T: Bar>(_x: T) { }
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 2 previous errors
+
+Some errors occurred: E0277, E0308.
+For more information about an error, try `rustc --explain E0277`.

src/test/ui/consts/const-size_of-cycle.stderr

@@ -10,7 +10,7 @@ note: ...which requires const-evaluating `Foo::bytes::{{constant}}`...
 LL |     intrinsics::size_of::<T>()
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^
 note: ...which requires computing layout of `Foo`...
-note: ...which requires normalizing `ParamEnvAnd { param_env: ParamEnv { caller_bounds: [], reveal: All }, value: [u8; _] }`...
+note: ...which requires normalizing `ParamEnvAnd { param_env: ParamEnv { caller_bounds: [], reveal: All, def_id: None }, value: [u8; _] }`...
 note: ...which requires const-evaluating + checking `Foo::bytes::{{constant}}`...
   --> $DIR/const-size_of-cycle.rs:6:17
    |

src/test/ui/issues/issue-44415.stderr

@@ -10,7 +10,7 @@ note: ...which requires const-evaluating `Foo::bytes::{{constant}}`...
 LL |     bytes: [u8; unsafe { intrinsics::size_of::<Foo>() }],
    |                          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 note: ...which requires computing layout of `Foo`...
-note: ...which requires normalizing `ParamEnvAnd { param_env: ParamEnv { caller_bounds: [], reveal: All }, value: [u8; _] }`...
+note: ...which requires normalizing `ParamEnvAnd { param_env: ParamEnv { caller_bounds: [], reveal: All, def_id: None }, value: [u8; _] }`...
 note: ...which requires const-evaluating + checking `Foo::bytes::{{constant}}`...
   --> $DIR/issue-44415.rs:6:17
    |