refactor: Canonicalizer: run getFunInfo on expression, not key (lea…

…nprover#3875)

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

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