From f3526ca18fa6e33306ccd1b8bd6c6af8f7dd3dc9 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Tue, 8 Oct 2019 10:14:56 -0700
Subject: [PATCH] fix: handle no instances for a typeclass goal

---
 library/Init/Lean/TypeClass/Synth.lean | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean
index 44c59ca56d..325d1c4d57 100644
--- a/library/Init/Lean/TypeClass/Synth.lean
+++ b/library/Init/Lean/TypeClass/Synth.lean
@@ -216,19 +216,13 @@ do lookupStatus ← get >>= λ ϕ => pure $ ϕ.env.find instName;
 def generate : TCMethod Unit :=
 do gNode ← get >>= λ ϕ => pure ϕ.generatorStack.back;
    match gNode.remainingInstances with
-   | []                  => throw "[generate] gNode.remainingInstances.isEmpty"
+   | []          => modify $ λ ϕ => { generatorStack := ϕ.generatorStack.pop, .. ϕ }
    | inst::insts => do
      ⟨instTE, ctx⟩ ← match inst with
                      | Instance.const n     => constNameToTypedExpr gNode.ctx n
                      | Instance.lDecl lDecl => throw "local instances not yet supported";
      result : Option (Context × List Expr) ← tryResolve ctx gNode.futureAnswer instTE;
-     nextGeneratorStack ←
-       if insts.isEmpty
-       then get >>= λ ϕ => pure ϕ.generatorStack.pop
-       else get >>= λ ϕ => pure $ ϕ.generatorStack.modify
-                                  (ϕ.generatorStack.size-1)
-                                  (λ gNode => { remainingInstances := insts .. gNode });
-     modify $ λ ϕ => { generatorStack := nextGeneratorStack, .. ϕ };
+     modify $ λ ϕ => { generatorStack := ϕ.generatorStack.modify (ϕ.generatorStack.size-1) (λ gNode => { remainingInstances := insts .. gNode }) .. ϕ };
      match result with
      | none => pure ()
      | some (ctx, newMVars) => newConsumerNode gNode.toNode ctx newMVars