max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: handle no instances for a typeclass goal

Browse source
This commit is contained in:
Daniel Selsam 2019-10-08 10:14:56 -07:00 • committed by Leonardo de Moura
parent 8207e05b0a
commit f3526ca18f
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/Init/Lean/TypeClass/Synth.lean
View file

@ -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