From f574cdf5e0b0b00c5dcd7b595f4805b4e0cb380c Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Fri, 8 Nov 2019 13:48:50 -0800
Subject: [PATCH] feat: fresh contexts for each new subgoal

---
 library/Init/Lean/TypeClass/Synth.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index 1da43324fd..ea0888ec19 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -104,17 +104,18 @@ def quickIsClass (env : Environment) : Expr → Option (Option Name)
 | _            => some none
 
 def newSubgoal (waiter : Waiter) (ctx : Context) (anormSubgoal mvar : Expr) : TCMethod Unit :=
-do let mvarType := ctx.eInfer mvar;
+do let mvarType := ctx.eInstantiate (ctx.eInfer mvar);
    isClassStatus ← get >>= λ ϕ => pure $ quickIsClass ϕ.env mvarType;
    match isClassStatus with
    | none      => throw $ "quickIsClass not sufficient to show `" ++ toString mvarType ++ "` is a class"
    | some none => throw $ "found non-class goal `" ++ toString mvarType ++ "`"
    | some (some n) => do
+     let ⟨newVal, newType, newCtx⟩ := Context.internalize ctx mvar mvarType {};
      gNode ← get >>= λ ϕ => pure {
        GeneratorNode .
-       ctx                := ctx,
+       ctx                := newCtx,
        anormSubgoal       := anormSubgoal,
-       futureAnswer       := ⟨mvar, mvarType⟩,
+       futureAnswer       := ⟨newVal, newType⟩,
        remainingInstances := (getClassInstances ϕ.env n).map Instance.const
      };
      let tableEntry : TableEntry := { waiters := #[waiter] };