chore: improve eqvTypes

src/Lean/Compiler/LCNF/InferType.lean

@@ -416,6 +416,9 @@ We have that `List Nat` and `List ◾` are compatible types, but they are not eq
 partial def eqvTypes (a b : Expr) : Bool :=
   if a == b then
     true
+  else if a.isErased && b.isErased then
+    -- `◾ α` is equivalent to `◾`
+    true
   else
     let a' := a.headBeta
     let b' := b.headBeta

src/Lean/Compiler/LCNF/Passes.lean

@@ -113,5 +113,6 @@ builtin_initialize
 
 builtin_initialize
   registerTraceClass `Compiler.saveBase (inherited := true)
+  registerTraceClass `Compiler.trace (inherited := true)
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Simp/InlineProj.lean

@@ -43,7 +43,7 @@ partial def inlineProjInst? (e : Expr) (expectedType : Expr) : SimpM (Option (Ar
   let (fvarId?, decls) ← visit s [i] |>.run |>.run #[]
   if let some fvarId := fvarId? then
     let type ← getType fvarId
-    if type.isErased || eqvTypes expectedType type then
+    if expectedType.isErased || type.isErased || eqvTypes expectedType type then
       return some (decls, fvarId)
     else
       let cast ← mkLcCast (.fvar fvarId) expectedType