From 36db04072223de75024ed39e46ca5698d9cc549b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 10 Apr 2024 22:41:15 +0200 Subject: [PATCH] refactor: Canonicalizer: run `getFunInfo` on expression, not key (#3875) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Canonicalizer creates a “key” expression eliding certain information (implicit parameters, levels), and `getFunInfo` can be confused by these terms (in particular, wrong number of level parameters). By running `getFunInfo` on the original expression we avoid this, and can just put `[]` as the level list in the key. --- src/Lean/Meta/Canonicalizer.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean index bb715610927e..257d9b7c9171 100644 --- a/src/Lean/Meta/Canonicalizer.lean +++ b/src/Lean/Meta/Canonicalizer.lean @@ -84,8 +84,8 @@ private partial def mkKey (e : Expr) : CanonM Key := do let key ← match e with | .sort .. | .fvar .. | .bvar .. | .lit .. => pure { e := (← shareCommon e) } - | .const n ls => - pure { e := (← shareCommon (.const n (List.replicate ls.length levelZero))) } + | .const n _ => + pure { e := (← shareCommon (.const n [])) } | .mvar .. => -- We instantiate assigned metavariables because the -- pretty-printer also instantiates them. @@ -94,7 +94,7 @@ private partial def mkKey (e : Expr) : CanonM Key := do else mkKey eNew | .mdata _ a => mkKey a | .app .. => - let f := (← mkKey e.getAppFn).e + let f := e.getAppFn if f.isMVar then let eNew ← instantiateMVars e unless eNew == e do @@ -109,7 +109,8 @@ private partial def mkKey (e : Expr) : CanonM Key := do pure (mkSort 0) -- some dummy value for erasing implicit else pure (← mkKey arg).e - pure { e := (← shareCommon (mkAppN f args)) } + let f' := (← mkKey f).e + pure { e := (← shareCommon (mkAppN f' args)) } | .lam n t b i => pure { e := (← shareCommon (.lam n (← mkKey t).e (← mkKey b).e i)) } | .forallE n t b i =>