feat: on "type mismatch" errors, expose differences in functions and …

…pi types

Example: Normally subtype notation pretty prints as `{ x // x > 0 }`, but now the difference in domains is exposed:
```
example : {x : Nat // x > 0} :=
  (sorry : {x : Int // x > 0})
/-
error: type mismatch
  sorry
has type
  { x : Int // x > 0 } : Type
but is expected to have type
  { x : Nat // x > 0 } : Type
-/
```

src/Lean/Expr.lean

@@ -1836,6 +1836,20 @@ The delaborator uses `pp` options.
 def setPPUniverses (e : Expr) (flag : Bool) :=
   e.setOption `pp.universes flag
 
+/--
+Annotate `e` with `pp.piBinderTypes := flag`
+The delaborator uses `pp` options.
+-/
+def setPPPiBinderTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.piBinderTypes flag
+
+/--
+Annotate `e` with `pp.funBinderTypes := flag`
+The delaborator uses `pp` options.
+-/
+def setPPFunBinderTypes (e : Expr) (flag : Bool) :=
+  e.setOption `pp.funBinderTypes flag
+
 /--
 Annotate `e` with `pp.explicit := flag`
 The delaborator uses `pp` options.

src/Lean/Meta/Check.lean

@@ -37,8 +37,9 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do
   | _                    => throwFunctionExpected f
 
 /--
-Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true` to
-expose "implicit" differences. For example, suppose `a` and `b` are of the form
+Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true`
+and other `pp` options to expose "implicit" differences.
+For example, suppose `a` and `b` are of the form
 ```lean
 @HashMap Nat Nat eqInst hasInst1
 @HashMap Nat Nat eqInst hasInst2
@@ -67,7 +68,8 @@ has type
 but is expected to have type
   @HashMap Nat Nat eqInst hasInst2
 ```
-Remark: this method implements a simple heuristic, we should extend it as we find other counterintuitive
+
+Remark: this method implements simple heuristics; we should extend it as we find other counterintuitive
 error messages.
 -/
 partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
@@ -142,6 +144,28 @@ where
             return (a, b)
           else
             return (a.setPPExplicit true, b.setPPExplicit true)
+      | .forallE na ta ba bia, .forallE nb tb bb bib =>
+        if !(← isDefEq ta tb) then
+          let (ta, tb) ← visit ta tb
+          let a := Expr.forallE na ta ba bia
+          let b := Expr.forallE nb tb bb bib
+          return (a.setPPPiBinderTypes true, b.setPPPiBinderTypes true)
+        else
+          -- Then bodies must not be defeq.
+          withLocalDeclD na ta fun arg => do
+            let (ba', bb') ← visit (ba.instantiate1 arg) (bb.instantiate1 arg)
+            return (Expr.forallE na ta (ba'.abstract #[arg]) bia, Expr.forallE nb tb (bb'.abstract #[arg]) bib)
+      | .lam na ta ba bia, .lam nb tb bb bib =>
+        if !(← isDefEq ta tb) then
+          let (ta, tb) ← visit ta tb
+          let a := Expr.lam na ta ba bia
+          let b := Expr.lam nb tb bb bib
+          return (a.setPPFunBinderTypes true, b.setPPFunBinderTypes true)
+        else
+          -- Then bodies must not be defeq.
+          withLocalDeclD na ta fun arg => do
+            let (ba', bb') ← visit (ba.instantiate1 arg) (bb.instantiate1 arg)
+            return (Expr.lam na ta (ba'.abstract #[arg]) bia, Expr.lam nb tb (bb'.abstract #[arg]) bib)
       | _, _ => return (a, b)
     catch _ =>
       return (a, b)

tests/lean/run/addPPExplicitToExposeDiff.lean

@@ -105,3 +105,60 @@ but is expected to have type
 #guard_msgs in example : (0 : Nat → Nat) 1 = (0 : Nat → Nat) 1 := by
   exact Eq.refl ((0 : Nat → Int) 1)
 end
+
+/-!
+Exposes differences in pi type domains
+-/
+/--
+error: type mismatch
+  fun h => trivial
+has type
+  (1 : Int) = 1 → True : Prop
+but is expected to have type
+  (1 : Nat) = 1 → True : Prop
+-/
+#guard_msgs in example : (1 : Nat) = 1 → True :=
+  fun (h : (1 : Int) = 1) => trivial
+
+/-!
+Exposes differences in pi type codomains
+-/
+/--
+error: type mismatch
+  fun h => rfl
+has type
+  True → (1 : Int) = 1 : Prop
+but is expected to have type
+  True → (1 : Nat) = 1 : Prop
+-/
+#guard_msgs in example : True → (1 : Nat) = 1 :=
+  (fun h => rfl : True → (1 : Int) = 1)
+
+/-!
+Exposes differences in fun domains
+-/
+/--
+error: type mismatch
+  sorry
+has type
+  { x : Int // x > 0 } : Type
+but is expected to have type
+  { x : Nat // x > 0 } : Type
+-/
+#guard_msgs in example : {x : Nat // x > 0} :=
+  (sorry : {x : Int // x > 0})
+
+/-!
+Exposes differences in fun values
+-/
+/--
+error: type mismatch
+  sorry
+has type
+  { x // @decide (p x) (d2 x) = true } : Type
+but is expected to have type
+  { x // @decide (p x) (d1 x) = true } : Type
+-/
+#guard_msgs in example (p : Nat → Prop) (d1 d2 : DecidablePred p) :
+    {x : Nat // @decide _ (d1 x) = true} :=
+  (sorry : {x : Nat // @decide _ (d2 x) = true})