From 5fb1680f7196a7fed7f43e8a761c2441f6986b75 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Sat, 8 Jun 2024 21:44:52 -0400 Subject: [PATCH] Inhabitation reasoning bug fix --- Duper/Util/TypeInhabitationReasoning.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Duper/Util/TypeInhabitationReasoning.lean b/Duper/Util/TypeInhabitationReasoning.lean index 81e68a4..5789d8c 100644 --- a/Duper/Util/TypeInhabitationReasoning.lean +++ b/Duper/Util/TypeInhabitationReasoning.lean @@ -270,6 +270,8 @@ def removeVanishedVarsHelper (c : Clause) (verifiedInhabitedTypes : abstractedMV potentiallyUninhabitedTypes := abstractedType :: potentiallyUninhabitedTypes resPotentiallyVacuous := true | some _ => -- Don't remove mvarId because it appears in clause body + let abstractedType ← abstractMVars mvarType -- Need to redefine `abstractedType` because `Meta.findInstance` can modify metavariables that appear in `mvarType` + trace[duper.typeInhabitationReasoning.debug] "Adding abstractedType {abstractedType.expr} corresponding to {mvarType} to verifiedInhabitedtypes" verifiedInhabitedTypes := abstractedType :: verifiedInhabitedTypes else if verifiedInhabitedTypes.contains abstractedType then @@ -298,6 +300,8 @@ def removeVanishedVarsHelper (c : Clause) (verifiedInhabitedTypes : abstractedMV resPotentiallyVacuous := true | some _ => trace[duper.typeInhabitationReasoning.debug] "{mvar} is to be removed because Meta.findInstance found an instance for {mvarType}" + let abstractedType ← abstractMVars mvarType -- Need to redefine `abstractedType` because `Meta.findInstance` can modify metavariables that appear in `mvarType` + trace[duper.typeInhabitationReasoning.debug] "Adding abstractedType {abstractedType.expr} corresponding to {mvarType} to verifiedInhabitedtypes" verifiedInhabitedTypes := abstractedType :: verifiedInhabitedTypes mvarIdsToRemove := mvarId :: mvarIdsToRemove if mvarIdsToRemove.isEmpty then