add type reduction feature

Auto/Lib/MetaExtra.lean

@@ -9,6 +9,25 @@ namespace Auto
 
 def Meta.isDefEqD (t s : Expr) : MetaM Bool := Meta.withDefault <| Meta.isDefEq t s
 
+def Meta.whnfNondependentForall (e : Expr) : MetaM Expr := do
+  let e' ← Meta.whnf e
+  match e' with
+  | .forallE _ _ body _ =>
+    if body.hasLooseBVar 0 then
+      return e
+    else
+      return e'
+  | _ => return e
+
+partial def Meta.normalizeNondependentForall (e : Expr) : MetaM Expr := do
+  let e' ← whnfNondependentForall e
+  match e' with
+  | .forallE name ty body bi =>
+    let ty' ← normalizeNondependentForall ty
+    let body' ← normalizeNondependentForall body
+    return .forallE name ty' body' bi
+  | _ => return e
+
 def Meta.withoutMVarAssignments (m : MetaM α) : MetaM α := do
   let mctx ← getMCtx
   Meta.withMCtx {mctx with eAssignment := {}, lAssignment := {}} m

Auto/Translation/LamReif.lean

@@ -1011,7 +1011,7 @@ private def reifTypeAux : Expr → ReifM LamSort
 | e => processTypeExpr e
 
 def reifType (e : Expr) : ReifM LamSort := do
-  let e ← prepReduceExpr e
+  let e ← prepReduceTypeForall e
   reifTypeAux e
 
 def newTermExpr (e : Expr) : ReifM LamTerm := do

Auto/Translation/Monomorphization.lean

@@ -57,16 +57,6 @@ register_option auto.mono.termLikeDefEq.maxHeartbeats : Nat := {
   descr := "Heartbeats allocated to each unification of term-like expression"
 }
 
-register_option auto.mono.tyRed.mode : Meta.TransparencyMode := {
-  defValue := .reducible
-  descr := "Transparency level used when reducing types"
-}
-
-register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := {
-  defValue := .default
-  descr := "Transparency level used when testing definitional equality of types"
-}
-
 namespace Auto
 
 inductive MonoMode where
@@ -842,8 +832,7 @@ namespace FVarRep
 
   /-- Return : (reduce(e), whether reduce(e) contain bfvars) -/
   def processType (e : Expr) : FVarRepM (Expr × Bool) := do
-    let mode := auto.mono.tyRed.mode.get (← getOptions)
-    let e ← MetaState.runMetaM <| prepReduceExprWithMode e mode
+    let e ← MetaState.runMetaM <| prepReduceTypeForall e
     let bfvarSet ← getBfvarSet
     -- If `e` contains no bound variables
     if !e.hasAnyFVar bfvarSet.contains then

Auto/Translation/Reduction.lean

@@ -1,5 +1,6 @@
 import Lean
 import Auto.Lib.ExprExtra
+import Auto.Lib.MetaExtra
 open Lean Meta
 
 private instance : ToString TransparencyMode where
@@ -23,6 +24,16 @@ register_option auto.redMode : TransparencyMode := {
   descr := "TransparencyMode used when reducing collected facts"
 }
 
+register_option auto.mono.tyRed.mode : Meta.TransparencyMode := {
+  defValue := .reducible
+  descr := "Transparency level used when reducing types. The default mode `reducible` does nothing."
+}
+
+register_option auto.mono.tyDefEq.mode : Meta.TransparencyMode := {
+  defValue := .default
+  descr := "Transparency level used when testing definitional equality of types"
+}
+
 namespace Auto
 
 def unfoldProj (e : Expr) : MetaM Expr :=
@@ -79,4 +90,9 @@ def prepReduceDefeq (type : Expr) : MetaM (Option Expr) := do
     let eq' := Lean.mkApp3 (.const ``Eq lvls) ty lhs rhs
     return .some (← mkForallFVars xs eq')
 
+def prepReduceTypeForall (e : Expr) : MetaM Expr := do
+  let e ← prepReduceExpr e
+  let mode := auto.mono.tyRed.mode.get (← getOptions)
+  Meta.withTransparency mode <| Meta.normalizeNondependentForall e
+
 end Auto