diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 4fa4a70993d..e62eb88a4f5 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -85,6 +85,8 @@ impl Debug for Ty {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match self {
             Ty::BoundVar(depth) => write!(fmt, "^{}", depth),
+            Ty::Dyn(clauses) => write!(fmt, "{:?}", clauses),
+            Ty::Opaque(clauses) => write!(fmt, "{:?}", clauses),
             Ty::InferenceVar(var) => write!(fmt, "{:?}", var),
             Ty::Apply(apply) => write!(fmt, "{:?}", apply),
             Ty::Projection(proj) => write!(fmt, "{:?}", proj),
diff --git a/chalk-ir/src/fold.rs b/chalk-ir/src/fold.rs
index 6aea130e0fd..367feb480b4 100644
--- a/chalk-ir/src/fold.rs
+++ b/chalk-ir/src/fold.rs
@@ -341,6 +341,8 @@ pub fn super_fold_ty(folder: &mut dyn Folder, ty: &Ty, binders: usize) -> Fallib
                 Ok(Ty::BoundVar(depth))
             }
         }
+        Ty::Dyn(ref clauses) => Ok(Ty::Dyn(clauses.fold_with(folder, binders)?)),
+        Ty::Opaque(ref clauses) => Ok(Ty::Opaque(clauses.fold_with(folder, binders)?)),
         Ty::InferenceVar(var) => folder.fold_inference_ty(var, binders),
         Ty::Apply(ref apply) => {
             let ApplicationTy {
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index 7cc9b8d2b10..0eeced70f2a 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -25,7 +25,7 @@ macro_rules! impl_debugs {
 use crate::cast::Cast;
 use crate::fold::shift::Shift;
 use crate::fold::{
-    DefaultInferenceFolder, DefaultPlaceholderFolder, DefaultTypeFolder, Fold, FreeVarFolder,
+    DefaultInferenceFolder, DefaultPlaceholderFolder, DefaultTypeFolder, Fold, FreeVarFolder, Subst,
 };
 use chalk_engine::fallible::*;
 use lalrpop_intern::InternedString;
@@ -235,6 +235,41 @@ pub enum Ty {
     /// an empty list).
     Apply(ApplicationTy),
 
+    /// A "dyn" type is a trait object type created via the "dyn Trait" syntax.
+    /// In the chalk parser, the traits that the object represents is parsed as
+    /// a QuantifiedInlineBound, and is then changed to a list of where clauses
+    /// during lowering.
+    ///
+    /// See the `Opaque` variant for a discussion about the use of
+    /// binders here.
+    Dyn(Binders<Vec<QuantifiedWhereClause>>),
+
+    /// An "opaque" type is one that is created via the "impl Trait" syntax.
+    /// They are named so because the concrete type implementing the trait
+    /// is unknown, and hence the type is opaque to us. The only information
+    /// that we know of is that this type implements the traits listed by the
+    /// user.
+    ///
+    /// The "binder" here represents the unknown self type. So, a type like
+    /// `impl for<'a> Fn(&'a u32)` would be represented with two-levels of
+    /// binder, as "depicted" here:
+    ///
+    /// ```notrust
+    /// exists<type> {
+    ///    vec![
+    ///        // A QuantifiedWhereClause:
+    ///        forall<region> { ^1: Fn(&^0 u32) }
+    ///    ]
+    /// }
+    /// ```
+    ///
+    /// The outer `exists<type>` binder indicates that there exists
+    /// some type that meets the criteria within, but that type is not
+    /// known. It is referenced within the type using `^1`, indicating
+    /// a bound type with debruijn index 1 (i.e., skipping through one
+    /// level of binder).
+    Opaque(Binders<Vec<QuantifiedWhereClause>>),
+
     /// A "projection" type corresponds to an (unnormalized)
     /// projection like `<P0 as Trait<P1..Pn>>::Foo`. Note that the
     /// trait and all its parameters are fully known.
@@ -788,6 +823,20 @@ impl<T> Binders<T> {
     }
 }
 
+impl<T> Binders<T>
+where
+    T: Fold,
+{
+    /// Substitute `parameters` for the variables introduced by these
+    /// binders. So if the binders represent (e.g.) `<X, Y> { T }` and
+    /// parameters is the slice `[A, B]`, then returns `[X => A, Y =>
+    /// B] T`.
+    pub fn substitute(&self, parameters: &[Parameter]) -> T::Result {
+        assert_eq!(self.binders.len(), parameters.len());
+        Subst::apply(parameters, &self.value)
+    }
+}
+
 /// Allows iterating over a Binders<Vec<T>>, for instance.
 /// Each element will include the same set of parameter bounds.
 impl<V: IntoIterator> IntoIterator for Binders<V> {
diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs
index 2f8270fc689..3b0588950c6 100644
--- a/chalk-parse/src/ast.rs
+++ b/chalk-parse/src/ast.rs
@@ -153,6 +153,12 @@ pub enum Ty {
     Id {
         name: Identifier,
     },
+    Dyn {
+        bounds: Vec<QuantifiedInlineBound>,
+    },
+    Opaque {
+        bounds: Vec<QuantifiedInlineBound>,
+    },
     Apply {
         name: Identifier,
         args: Vec<Parameter>,
diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop
index e1c6b9a0a1c..d0290e6b795 100644
--- a/chalk-parse/src/parser.lalrpop
+++ b/chalk-parse/src/parser.lalrpop
@@ -171,6 +171,12 @@ pub Ty: Ty = {
 
 TyWithoutFor: Ty = {
     <n:Id> => Ty::Id { name: n},
+    "dyn" <b:Plus<QuantifiedInlineBound>> => Ty::Dyn {
+        bounds: b,
+    },
+    "impl" <b:Plus<QuantifiedInlineBound>> => Ty::Opaque {
+        bounds: b,
+    },
     <n:Id> "<" <a:Comma<Parameter>> ">" => Ty::Apply { name: n, args: a },
     <p:ProjectionTy> => Ty::Projection { proj: p },
     "(" <Ty> ")",
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index 1cc7d069902..6cad841d8a3 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -167,6 +167,28 @@ fn program_clauses_that_could_match(
                 }
             }
 
+            // If the self type is `dyn Foo` (or `impl Foo`), then we generate clauses like:
+            //
+            // ```notrust
+            // Implemented(dyn Foo: Foo)
+            // ```
+            //
+            // FIXME. This is presently rather wasteful, in that we
+            // don't check that the `dyn Foo: Foo` trait is relevant
+            // to the goal `goal` that we are actually *trying* to
+            // prove (though there is some later code that will screen
+            // out irrelevant stuff). In other words, we might be
+            // trying to prove `dyn Foo: Bar`, in which case the clause
+            // for `dyn Foo: Foo` is not particularly relevant.
+            match trait_ref.self_type_parameter() {
+                Some(Ty::Opaque(qwc)) | Some(Ty::Dyn(qwc)) => {
+                    let self_ty = trait_ref.self_type_parameter().unwrap(); // This cannot be None
+                    let wc = qwc.substitute(&[self_ty.cast()]);
+                    clauses.extend(wc.into_iter().casted());
+                }
+                _ => {}
+            }
+
             // TODO sized, unsize_trait, builtin impls?
         }
         DomainGoal::Holds(WhereClause::ProjectionEq(projection_predicate)) => {
@@ -246,8 +268,17 @@ fn push_program_clauses_for_associated_type_values_in_impls_of(
     }
 }
 
-/// Given the "self-type" of a domain goal, push potentially relevant program
-/// clauses.
+/// Examine `T` and push clauses that may be relevant to proving the
+/// following sorts of goals (and maybe others):
+///
+/// * `DomainGoal::WellFormed(T)`
+/// * `DomainGoal::IsUpstream(T)`
+/// * `DomainGoal::DownstreamType(T)`
+/// * `DomainGoal::IsFullyVisible(T)`
+/// * `DomainGoal::IsLocal(T)`
+///
+/// Note that the type `T` must not be an unbound inference variable;
+/// earlier parts of the logic should "flounder" in that case.
 fn match_ty(
     db: &dyn RustIrDatabase,
     environment: &Arc<Environment>,
@@ -268,6 +299,7 @@ fn match_ty(
         Ty::ForAll(quantified_ty) => match_ty(db, environment, &quantified_ty.ty, clauses),
         Ty::BoundVar(_) => {}
         Ty::InferenceVar(_) => panic!("should have floundered"),
+        Ty::Dyn(_) | Ty::Opaque(_) => {}
     }
 }
 
diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs
index a86b89f836a..5589d2e1f4f 100644
--- a/chalk-solve/src/clauses/env_elaborator.rs
+++ b/chalk-solve/src/clauses/env_elaborator.rs
@@ -61,6 +61,11 @@ impl<'db, 'set> EnvElaborator<'db, 'set> {
             Ty::Projection(projection_ty) => {
                 self.visit_projection_ty(projection_ty);
             }
+
+            // FIXME(#203) -- We haven't fully figured out the implied
+            // bounds story around object and impl trait types.
+            Ty::Dyn(_) | Ty::Opaque(_) => (),
+
             Ty::ForAll(_) | Ty::BoundVar(_) | Ty::InferenceVar(_) => (),
         }
         self.round.extend(clauses);
diff --git a/chalk-solve/src/infer/unify.rs b/chalk-solve/src/infer/unify.rs
index be1c76520e5..c04d5d573fa 100644
--- a/chalk-solve/src/infer/unify.rs
+++ b/chalk-solve/src/infer/unify.rs
@@ -105,6 +105,8 @@ impl<'t> Unifier<'t> {
         );
 
         match (a, b) {
+            // Unifying two inference variables: unify them in the underlying
+            // ena table.
             (&Ty::InferenceVar(var1), &Ty::InferenceVar(var2)) => {
                 debug!("unify_ty_ty: unify_var_var({:?}, {:?})", var1, var2);
                 let var1 = EnaVariable::from(var1);
@@ -116,21 +118,33 @@ impl<'t> Unifier<'t> {
                     .expect("unification of two unbound variables cannot fail"))
             }
 
+            // Unifying an inference variables with a non-inference variable.
             (&Ty::InferenceVar(var), ty @ &Ty::Apply(_))
             | (ty @ &Ty::Apply(_), &Ty::InferenceVar(var))
+            | (&Ty::InferenceVar(var), ty @ &Ty::Opaque(_))
+            | (ty @ Ty::Opaque(_), &Ty::InferenceVar(var))
+            | (&Ty::InferenceVar(var), ty @ &Ty::Dyn(_))
+            | (ty @ &Ty::Dyn(_), &Ty::InferenceVar(var))
             | (&Ty::InferenceVar(var), ty @ &Ty::ForAll(_))
             | (ty @ &Ty::ForAll(_), &Ty::InferenceVar(var)) => self.unify_var_ty(var, ty),
 
+            // Unifying `forall<X> { T }` with some other forall type `forall<X> { U }`
             (&Ty::ForAll(ref quantified_ty1), &Ty::ForAll(ref quantified_ty2)) => {
                 self.unify_forall_tys(quantified_ty1, quantified_ty2)
             }
 
-            (&Ty::ForAll(ref quantified_ty), apply_ty @ &Ty::Apply(_))
-            | (apply_ty @ &Ty::Apply(_), &Ty::ForAll(ref quantified_ty)) => {
-                self.unify_forall_apply(quantified_ty, apply_ty)
+            // Unifying `forall<X> { T }` with some other type `U`
+            (&Ty::ForAll(ref quantified_ty), other_ty @ &Ty::Apply(_))
+            | (&Ty::ForAll(ref quantified_ty), other_ty @ &Ty::Dyn(_))
+            | (&Ty::ForAll(ref quantified_ty), other_ty @ &Ty::Opaque(_))
+            | (other_ty @ &Ty::Apply(_), &Ty::ForAll(ref quantified_ty))
+            | (other_ty @ &Ty::Dyn(_), &Ty::ForAll(ref quantified_ty))
+            | (other_ty @ &Ty::Opaque(_), &Ty::ForAll(ref quantified_ty)) => {
+                self.unify_forall_other(quantified_ty, other_ty)
             }
 
             (&Ty::Apply(ref apply1), &Ty::Apply(ref apply2)) => {
+                // Cannot unify (e.g.) some struct type `Foo` and some struct type `Bar`
                 if apply1.name != apply2.name {
                     return Err(NoSolution);
                 }
@@ -138,13 +152,37 @@ impl<'t> Unifier<'t> {
                 Zip::zip_with(self, &apply1.parameters, &apply2.parameters)
             }
 
+            // Cannot unify (e.g.) some struct type `Foo` and an `impl Trait` type
+            (&Ty::Apply(_), &Ty::Opaque(_)) | (&Ty::Opaque(_), &Ty::Apply(_)) => {
+                return Err(NoSolution);
+            }
+
+            // Cannot unify (e.g.) some struct type `Foo` and a `dyn Trait` type
+            (&Ty::Apply(_), &Ty::Dyn(_)) | (&Ty::Dyn(_), &Ty::Apply(_)) => {
+                return Err(NoSolution);
+            }
+
+            // Cannot unify (e.g.) some `dyn Trait` and some `impl Trait` type
+            (&Ty::Dyn(..), &Ty::Opaque(..)) | (&Ty::Opaque(..), &Ty::Dyn(..)) => {
+                return Err(NoSolution);
+            }
+
+            (&Ty::Opaque(ref qwc1), &Ty::Opaque(ref qwc2))
+            | (&Ty::Dyn(ref qwc1), &Ty::Dyn(ref qwc2)) => Zip::zip_with(self, qwc1, qwc2),
+
+            // Unifying an associated type projection `<T as
+            // Trait>::Item` with some other type `U`.
             (ty @ &Ty::Apply(_), &Ty::Projection(ref proj))
             | (ty @ &Ty::ForAll(_), &Ty::Projection(ref proj))
             | (ty @ &Ty::InferenceVar(_), &Ty::Projection(ref proj))
+            | (ty @ &Ty::Dyn(_), &Ty::Projection(ref proj))
+            | (ty @ &Ty::Opaque(_), &Ty::Projection(ref proj))
             | (&Ty::Projection(ref proj), ty @ &Ty::Projection(_))
             | (&Ty::Projection(ref proj), ty @ &Ty::Apply(_))
             | (&Ty::Projection(ref proj), ty @ &Ty::ForAll(_))
-            | (&Ty::Projection(ref proj), ty @ &Ty::InferenceVar(_)) => {
+            | (&Ty::Projection(ref proj), ty @ &Ty::InferenceVar(_))
+            | (&Ty::Projection(ref proj), ty @ &Ty::Dyn(_))
+            | (&Ty::Projection(ref proj), ty @ &Ty::Opaque(_)) => {
                 self.unify_projection_ty(proj, ty)
             }
 
@@ -186,6 +224,12 @@ impl<'t> Unifier<'t> {
         self.sub_unify(ty1, ty2)
     }
 
+    /// Unify an associated type projection `proj` like `<T as Trait>::Item` with some other
+    /// type `ty` (which might also be a projection). Creates a goal like
+    ///
+    /// ```notrust
+    /// ProjectionEq(<T as Trait>::Item = U)
+    /// ```
     fn unify_projection_ty(&mut self, proj: &ProjectionTy, ty: &Ty) -> Fallible<()> {
         Ok(self.goals.push(InEnvironment::new(
             self.environment,
@@ -197,7 +241,11 @@ impl<'t> Unifier<'t> {
         )))
     }
 
-    fn unify_forall_apply(&mut self, ty1: &QuantifiedTy, ty2: &Ty) -> Fallible<()> {
+    /// Unifying `forall<X> { T }` with some other type `U` --
+    /// to do so, we create a fresh placeholder `P` for `X` and
+    /// see if `[X/Px] T` can be unified with `U`. This should
+    /// almost never be true, actually, unless `X` is unused.
+    fn unify_forall_other(&mut self, ty1: &QuantifiedTy, ty2: &Ty) -> Fallible<()> {
         let ui = self.table.new_universe();
         let lifetimes1: Vec<_> = (0..ty1.num_binders)
             .map(|idx| Lifetime::Placeholder(PlaceholderIndex { ui, idx }).cast())
@@ -209,6 +257,12 @@ impl<'t> Unifier<'t> {
         self.sub_unify(ty1, ty2)
     }
 
+    /// Unify an inference variable `var` with some non-inference
+    /// variable `ty`, just bind `var` to `ty`. But we must enforce two conditions:
+    ///
+    /// - `var` does not appear inside of `ty` (the standard `OccursCheck`)
+    /// - `ty` does not reference anything in a lifetime that could not be named in `var`
+    ///   (the extended `OccursCheck` created to handle universes)
     fn unify_var_ty(&mut self, var: InferenceVar, ty: &Ty) -> Fallible<()> {
         debug!("unify_var_ty(var={:?}, ty={:?})", var, ty);
 
diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs
index e295d449bca..40cc3800d84 100644
--- a/chalk-solve/src/solve/slg.rs
+++ b/chalk-solve/src/solve/slg.rs
@@ -447,7 +447,11 @@ impl MayInvalidate {
             }
 
             // For everything else, be conservative here and just say we may invalidate.
-            (Ty::ForAll(_), _) | (Ty::Apply(_), _) | (Ty::Projection(_), _) => true,
+            (Ty::ForAll(_), _)
+            | (Ty::Dyn(_), _)
+            | (Ty::Opaque(_), _)
+            | (Ty::Apply(_), _)
+            | (Ty::Projection(_), _) => true,
         }
     }
 
diff --git a/chalk-solve/src/solve/slg/aggregate.rs b/chalk-solve/src/solve/slg/aggregate.rs
index f76517c66a9..7429578e523 100644
--- a/chalk-solve/src/solve/slg/aggregate.rs
+++ b/chalk-solve/src/solve/slg/aggregate.rs
@@ -178,11 +178,12 @@ impl<'infer> AntiUnifier<'infer> {
 
             // Ugh. Aggregating two types like `for<'a> fn(&'a u32,
             // &'a u32)` and `for<'a, 'b> fn(&'a u32, &'b u32)` seems
-            // kinda' hard. Don't try to be smart for now, just plop a
+            // kinda hard. Don't try to be smart for now, just plop a
             // variable in there and be done with it.
-            (Ty::BoundVar(_), Ty::BoundVar(_)) | (Ty::ForAll(_), Ty::ForAll(_)) => {
-                self.new_variable()
-            }
+            (Ty::BoundVar(_), Ty::BoundVar(_))
+            | (Ty::ForAll(_), Ty::ForAll(_))
+            | (Ty::Dyn(_), Ty::Dyn(_))
+            | (Ty::Opaque(_), Ty::Opaque(_)) => self.new_variable(),
 
             (Ty::Apply(apply1), Ty::Apply(apply2)) => {
                 self.aggregate_application_tys(apply1, apply2)
@@ -195,6 +196,8 @@ impl<'infer> AntiUnifier<'infer> {
             // Mismatched base kinds.
             (Ty::InferenceVar(_), _)
             | (Ty::BoundVar(_), _)
+            | (Ty::Dyn(_), _)
+            | (Ty::Opaque(_), _)
             | (Ty::ForAll(_), _)
             | (Ty::Apply(_), _)
             | (Ty::Projection(_), _) => self.new_variable(),
diff --git a/chalk-solve/src/solve/slg/resolvent.rs b/chalk-solve/src/solve/slg/resolvent.rs
index bfa9d16ee5d..0127cdfcc54 100644
--- a/chalk-solve/src/solve/slg/resolvent.rs
+++ b/chalk-solve/src/solve/slg/resolvent.rs
@@ -346,6 +346,10 @@ impl<'t> Zipper for AnswerSubstitutor<'t> {
 
             (Ty::Apply(answer), Ty::Apply(pending)) => Zip::zip_with(self, answer, pending),
 
+            (Ty::Dyn(answer), Ty::Dyn(pending)) | (Ty::Opaque(answer), Ty::Opaque(pending)) => {
+                Zip::zip_with(self, answer, pending)
+            }
+
             (Ty::Projection(answer), Ty::Projection(pending)) => {
                 Zip::zip_with(self, answer, pending)
             }
@@ -366,6 +370,8 @@ impl<'t> Zipper for AnswerSubstitutor<'t> {
 
             (Ty::BoundVar(_), _)
             | (Ty::Apply(_), _)
+            | (Ty::Dyn(_), _)
+            | (Ty::Opaque(_), _)
             | (Ty::Projection(_), _)
             | (Ty::ForAll(_), _) => panic!(
                 "structural mismatch between answer `{:?}` and pending goal `{:?}`",
diff --git a/chalk-solve/src/wf.rs b/chalk-solve/src/wf.rs
index 6e5a625eac1..5857ad856a5 100644
--- a/chalk-solve/src/wf.rs
+++ b/chalk-solve/src/wf.rs
@@ -70,6 +70,10 @@ impl FoldInputTypes for Ty {
                 accumulator.push(self.clone());
                 app.parameters.fold(accumulator);
             }
+            Ty::Dyn(qwc) | Ty::Opaque(qwc) => {
+                accumulator.push(self.clone());
+                qwc.fold(accumulator);
+            }
             Ty::Projection(proj) => {
                 accumulator.push(self.clone());
                 proj.parameters.fold(accumulator);
diff --git a/src/lowering.rs b/src/lowering.rs
index 57e50291db9..a507cc21611 100644
--- a/src/lowering.rs
+++ b/src/lowering.rs
@@ -3,6 +3,7 @@ use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::{self, ImplId, StructId, TraitId, TypeId, TypeKindId};
 use chalk_parse::ast::*;
 use chalk_rust_ir as rust_ir;
+use chalk_rust_ir::IntoWhereClauses;
 use chalk_rust_ir::{Anonymize, ToParameter};
 use failure::{Fail, Fallible};
 use itertools::Itertools;
@@ -64,6 +65,7 @@ enum LifetimeLookup {
 }
 
 const SELF: &str = "Self";
+const FIXME_SELF: &str = "__FIXME_SELF__";
 
 impl<'k> Env<'k> {
     fn lookup(&self, name: Identifier) -> Fallible<NameLookup> {
@@ -857,6 +859,30 @@ impl LowerTy for Ty {
                 NameLookup::Parameter(d) => Ok(chalk_ir::Ty::BoundVar(d)),
             },
 
+            Ty::Dyn { ref bounds } => Ok(chalk_ir::Ty::Dyn(env.in_binders(
+                // FIXME: Figure out a proper name for this type parameter
+                Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))),
+                |env| {
+                    Ok(bounds
+                        .lower(env)?
+                        .iter()
+                        .flat_map(|qil| qil.into_where_clauses(chalk_ir::Ty::BoundVar(0)))
+                        .collect())
+                },
+            )?)),
+
+            Ty::Opaque { ref bounds } => Ok(chalk_ir::Ty::Opaque(env.in_binders(
+                // FIXME: Figure out a proper name for this type parameter
+                Some(chalk_ir::ParameterKind::Ty(intern(FIXME_SELF))),
+                |env| {
+                    Ok(bounds
+                        .lower(env)?
+                        .iter()
+                        .flat_map(|qil| qil.into_where_clauses(chalk_ir::Ty::BoundVar(0)))
+                        .collect())
+                },
+            )?)),
+
             Ty::Apply { name, ref args } => {
                 let id = match env.lookup(name)? {
                     NameLookup::Type(id) => id,