From ee42c3ca561992fce95445faaa5c5355141cf87b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 27 Jun 2024 02:58:58 +0200
Subject: [PATCH] fix: discrepancy in the elaborators for `theorem`, `def`, and
 `example` (#4482)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When the type of a definition or example is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.

Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for definitions and
examples when their type was a proposition. This discrepancy often
confused users.

Additionally, we considered extending the above behavior whenever
the type of a definition is provided. That is, we would keep the
current behavior only if `: <type>` was omitted in a definition.
However, this proved to be too restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
  ⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
  ⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.

closes #4398

@semorrison @jcommelin: what do you think?
---
 src/Lean/Elab/MutualDef.lean                | 5 +----
 tests/lean/autoPPExplicit.lean.expected.out | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index fa9e3b0bf0..407174a33a 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -846,10 +846,7 @@ private def levelMVarToParamHeaders (views : Array DefView) (headers : Array Def
   let rec process : StateRefT Nat TermElabM (Array DefViewElabHeader) := do
     let mut newHeaders := #[]
     for view in views, header in headers do
-      -- Remark: we should consider using `pure view.kind.isTheorem <||> isProp header.type`, and
-      -- also handle definitions. We used the following approach because it is less disruptive to Mathlib.
-      -- Moreover, the type of most definitions are not propositions anyway.
-      if ← pure view.kind.isTheorem <||> (pure view.kind.isExample <&&> isProp header.type) then
+      if ← pure view.kind.isTheorem <||> isProp header.type then
         newHeaders ←
           withLevelNames header.levelNames do
             return newHeaders.push { header with type := (← levelMVarToParam header.type), levelNames := (← getLevelNames) }
diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out
index 445a458daa..680b9c24f7 100644
--- a/tests/lean/autoPPExplicit.lean.expected.out
+++ b/tests/lean/autoPPExplicit.lean.expected.out
@@ -5,4 +5,4 @@ argument
 has type
   Prop : Type
 but is expected to have type
-  α : Sort ?u
+  α : Sort u_1