From a8656c58128f2e6f11c09b47025baa1ad406333c Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sun, 15 Dec 2024 16:36:45 -0500
Subject: [PATCH] feat: generalize `panic` to `Sort` (#6333)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR generalizes the panic functions to a type of `Sort u` rather
than `Type u`. This better supports universe polymorphic types and
avoids confusing errors.

An minimal (but somewhat contrived) example of such a confusing error
is:

```lean
/-
stuck at solving universe constraint
  ?u.59+1 =?= max 1 ?u.7
while trying to unify
  Subtype.{?u.7} P : Sort (max 1 ?u.7)
with
  Subtype.{?u.7} P : Sort (max 1 ?u.7)
-/
def assertSubtype! {P : α → Prop} [Inhabited (Subtype P)] (a : α) [Decidable (P a)] : Subtype P := -- errors on :=
  if h : P a then
    ⟨a, h⟩
  else
    panic! "Property not satisified"
```
---
 src/Init/Prelude.lean | 4 ++--
 src/Init/Util.lean    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 20e29dc790..0d9514ae77 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2554,7 +2554,7 @@ When we reimplement the specializer, we may consider copying `inst` if it also
 occurs outside binders or if it is an instance.
 -/
 @[never_extract, extern "lean_panic_fn"]
-def panicCore {α : Type u} [Inhabited α] (msg : String) : α := default
+def panicCore {α : Sort u} [Inhabited α] (msg : String) : α := default
 
 /--
 `(panic "msg" : α)` has a built-in implementation which prints `msg` to
@@ -2568,7 +2568,7 @@ Because this is a pure function with side effects, it is marked as
 elimination and other optimizations that assume that the expression is pure.
 -/
 @[noinline, never_extract]
-def panic {α : Type u} [Inhabited α] (msg : String) : α :=
+def panic {α : Sort u} [Inhabited α] (msg : String) : α :=
   panicCore msg
 
 -- TODO: this be applied directly to `Inhabited`'s definition when we remove the above workaround
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 4f351a6bc9..7011f4b0ea 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -33,13 +33,13 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[noinline] private def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
-@[never_extract, inline] def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
+@[never_extract, inline] def panicWithPos {α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessage modName line col msg)
 
 @[noinline] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
-@[never_extract, inline] def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
+@[never_extract, inline] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessageWithDecl modName declName line col msg)
 
 @[extern "lean_ptr_addr"]