From 0b391f8eed657ac23abad15e5d6ae9a5c7852f11 Mon Sep 17 00:00:00 2001
From: Jack Huey <jack.huey@umassmed.edu>
Date: Tue, 8 Dec 2020 22:17:49 -0500
Subject: [PATCH] Forbid inference vars when getting program clauses

---
 chalk-engine/src/logic.rs  | 13 ++++++-------
 chalk-solve/src/clauses.rs | 11 ++++++++++-
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
index 504f03d726e..30cb0f1990c 100644
--- a/chalk-engine/src/logic.rs
+++ b/chalk-engine/src/logic.rs
@@ -322,13 +322,12 @@ impl<I: Interner> Forest<I> {
                         goal.canonical,
                     );
                 let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
-                // `canonical_goal` is a goal. We can simplify it
-                // into a series of *literals*, all of which must be
-                // true. Thus, in EWFS terms, we are effectively
-                // creating a single child of the `A :- A` goal that
-                // is like `A :- B, C, D` where B, C, and D are the
-                // simplified subgoals. You can think of this as
-                // applying built-in "meta program clauses" that
+                // The goal for this table is not a domain goal, so we instead
+                // simplify it into a series of *literals*, all of which must be
+                // true. Thus, in EWFS terms, we are effectively creating a
+                // single child of the `A :- A` goal that is like `A :- B, C, D`
+                // where B, C, and D are the simplified subgoals. You can think
+                // of this as applying built-in "meta program clauses" that
                 // reduce goals into Domain goals.
                 match Self::simplify_goal(context, &mut infer, subst, environment, goal) {
                     FallibleOrFloundered::Ok(ex_clause) => {
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index 2487c3586c7..ea6851338e2 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -403,6 +403,9 @@ fn program_clauses_that_could_match<I: Interner>(
             let trait_datum = db.trait_datum(trait_id);
 
             match self_ty.kind(interner) {
+                TyKind::InferenceVar(_, _) => {
+                    panic!("Inference vars not allowed when getting program clauses")
+                }
                 TyKind::Alias(alias) => {
                     // An alias could normalize to anything, including `dyn trait`
                     // or an opaque type, so push a clause that asks for the
@@ -590,6 +593,9 @@ fn program_clauses_that_could_match<I: Interner>(
                 let trait_datum = db.trait_datum(trait_id);
 
                 let self_ty = alias.self_type_parameter(interner);
+                if let TyKind::InferenceVar(_, _) = self_ty.kind(interner) {
+                    panic!("Inference vars not allowed when getting program clauses");
+                }
 
                 // Flounder if the self-type is unknown and the trait is non-enumerable.
                 //
@@ -847,6 +853,9 @@ fn match_ty<I: Interner>(
 ) -> Result<(), Floundered> {
     let interner = builder.interner();
     Ok(match ty.kind(interner) {
+        TyKind::InferenceVar(_, _) => {
+            panic!("Inference vars not allowed when getting program clauses")
+        }
         TyKind::Adt(adt_id, _) => builder
             .db
             .adt_datum(*adt_id)
@@ -890,7 +899,7 @@ fn match_ty<I: Interner>(
         TyKind::Function(_quantified_ty) => {
             builder.push_fact(WellFormed::Ty(ty.clone()));
         }
-        TyKind::BoundVar(_) | TyKind::InferenceVar(_, _) => return Err(Floundered),
+        TyKind::BoundVar(_) => return Err(Floundered),
         TyKind::Dyn(dyn_ty) => {
             // FIXME(#203)
             // - Object safety? (not needed with RFC 2027)