perf: simdutf8

This PR adds two validation checks to `addInstance` that provide early
feedback for common mistakes in instance declarations:

1. **Non-class instance check**: errors when an instance target type is
not a type class. This catches the common mistake of writing `instance`
for a plain structure. Previously handled by the `nonClassInstance`
linter in Batteries (`Batteries.Tactic.Lint.TypeClass`), this is now
checked directly at declaration time.

2. **Impossible argument check**: errors when an instance has arguments
that cannot be inferred by instance synthesis. Specifically, it flags
arguments that are not instance-implicit and do not appear in any
subsequent instance-implicit argument or in the return type. Previously
such instances would be silently accepted but could never be
synthesised.

Supersedes #13237 and #13333.

src/Init/Data/Order/LemmasExtra.lean

@@ -87,7 +87,7 @@ public theorem IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderO
 /--
 This lemma derives a `LawfulOrderLT α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α]
     (lt_iff_compare_eq_lt : ∀ a b : α, a < b ↔ compare a b = .lt) :
     LawfulOrderLT α where
   lt_iff a b := by
@@ -96,7 +96,7 @@ public instance LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [Law
 /--
 This lemma derives a `LawfulOrderBEq α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α]
     (beq_iff_compare_eq_eq : ∀ a b : α, a == b ↔ compare a b = .eq) :
     LawfulOrderBEq α where
   beq_iff_le_and_ge := by
@@ -105,7 +105,7 @@ public instance LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderInf α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE) :
     LawfulOrderInf α where
@@ -114,7 +114,7 @@ public instance LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMin α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α]
     (compare_min_isLE_iff : ∀ a b c : α,
         (compare a (min b c)).isLE ↔ (compare a b).isLE ∧ (compare a c).isLE)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
@@ -125,7 +125,7 @@ public instance LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderSup α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE) :
     LawfulOrderSup α where
@@ -134,7 +134,7 @@ public instance LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [L
 /--
 This lemma derives a `LawfulOrderMax α` instance from a property involving an `Ord α` instance.
 -/
-public instance LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
+public theorem LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α]
     (compare_max_isLE_iff : ∀ a b c : α,
         (compare (max a b) c).isLE ↔ (compare a c).isLE ∧ (compare b c).isLE)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :

src/Lean/Meta/Instances.lean

@@ -229,8 +229,33 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
 
   return synthed
 
+def checkImpossibleInstance (c : Expr) : MetaM Unit := do
+  let cTy ← inferType c
+  forallTelescopeReducing cTy fun args ty => do
+    let argTys ← args.mapM inferType
+    let impossibleArgs ← args.zipIdx.filterMapM fun (arg, i) => do
+      let fv := arg.fvarId!
+      if (← fv.getDecl).binderInfo.isInstImplicit then return none
+      if ty.containsFVar fv then return none
+      if argTys[i+1:].any (·.containsFVar fv) then return none
+      return some m!"{arg} : {← inferType arg}"
+    if impossibleArgs.isEmpty then return
+    let impossibleArgs := MessageData.joinSep impossibleArgs.toList ", "
+    throwError m!"Instance {c} has arguments "
+      ++ impossibleArgs
+      ++ " that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type."
+
+def checkNonClassInstance (declName : Name) (c : Expr) : MetaM Unit := do
+  let type ← inferType c
+  forallTelescopeReducing type fun _ target => do
+    unless (← isClass? target).isSome do
+      unless target.isSorry do
+      throwError m!"instance `{declName}` target `{target}` is not a type class."
+
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let c ← mkConstWithLevelParams declName
+  checkImpossibleInstance c
+  checkNonClassInstance declName c
   let keys ← mkInstanceKey c
   let status ← getReducibilityStatus declName
   unless status matches .reducible | .implicitReducible do

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -18,7 +18,7 @@ open Std.DHashMap.Internal
 
 namespace Std.DHashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
 
 end Std.DHashMap.Raw

src/Std/Data/DTreeMap/Raw/DecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DTreeMap.Internal.Impl
 
 namespace Std.DTreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := decidableEquiv t₁.1 t₂.1 h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/HashMap/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.DHashMap.Raw
 
 namespace Std.HashMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := DHashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/HashSet/RawDecidableEquiv.lean

@@ -19,7 +19,7 @@ open Std.HashMap.Raw
 
 namespace Std.HashSet.Raw
 
-instance instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+def instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
   let : Decidable (m₁.1 ~m m₂.1) := HashMap.Raw.instDecidableEquiv h₁.out h₂.out;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
 

src/Std/Data/TreeMap/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.DTreeMap.Raw
 
 namespace Std.TreeMap.Raw
 
-instance instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := DTreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/Std/Data/TreeSet/Raw/DecidableEquiv.lean

@@ -20,7 +20,7 @@ open Std.TreeMap.Raw
 
 namespace Std.TreeSet.Raw
 
-instance instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
+def instDecidableEquiv {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) : Decidable (t₁ ~m t₂) :=
   let : Ord α := ⟨cmp⟩;
   let : Decidable (t₁.inner ~m t₂.inner) := TreeMap.Raw.instDecidableEquiv h₁ h₂;
   decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩

src/runtime/CMakeLists.txt

@@ -5,6 +5,7 @@ set(
   mpz.cpp
   utf8.cpp
   object.cpp
+  simdutf.cpp
   apply.cpp
   exception.cpp
   interrupt.cpp

src/runtime/object.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "runtime/buffer.h"
 #include "runtime/io.h"
 #include "runtime/hash.h"
+#include "simdutf.h"
 
 #if defined(__GLIBC__) || defined(__APPLE__)
     #define LEAN_SUPPORTS_BACKTRACE 1
@@ -1978,15 +1979,16 @@ object * lean_mk_string_lossy_recover(char const * s, size_t sz, size_t pos, siz
 
 extern "C" LEAN_EXPORT object * lean_mk_string_from_bytes(char const * s, size_t sz) {
     size_t pos = 0, i = 0;
-    if (validate_utf8((const uint8_t *)s, sz, pos, i)) {
-        return lean_mk_string_unchecked(s, pos, i);
+    simdutf::result res = simdutf::validate_utf8_with_errors(s, sz);
+    if (res.error == simdutf::error_code::SUCCESS) {
+        return lean_mk_string_unchecked(s, sz, res.count);
     } else {
         return lean_mk_string_lossy_recover(s, sz, pos, i);
     }
 }
 
 extern "C" LEAN_EXPORT object * lean_mk_string_from_bytes_unchecked(char const * s, size_t sz) {
-    return lean_mk_string_unchecked(s, sz, utf8_strlen(s, sz));
+    return lean_mk_string_unchecked(s, sz, simdutf::count_utf8(s, sz));
 }
 
 extern "C" LEAN_EXPORT object * lean_mk_string(char const * s) {
@@ -2009,8 +2011,7 @@ extern "C" LEAN_EXPORT obj_res lean_string_from_utf8_unchecked(obj_arg a) {
 }
 
 extern "C" LEAN_EXPORT uint8 lean_string_validate_utf8(b_obj_arg a) {
-    size_t pos = 0, i = 0;
-    return validate_utf8(lean_sarray_cptr(a), lean_sarray_size(a), pos, i);
+    return simdutf::validate_utf8((const char*)lean_sarray_cptr(a), lean_sarray_size(a));
 }
 
 extern "C" LEAN_EXPORT obj_res lean_string_to_utf8(b_obj_arg s) {

src/runtime/utf8.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "runtime/debug.h"
 #include "runtime/optional.h"
+#include "runtime/simdutf.h"
 #include "runtime/utf8.h"
 
 namespace lean {

tests/compile/large_closure_bug.lean

@@ -68,10 +68,10 @@ def ExtractNonDet.bind :
     dsimp [Bind.bind, NonDetT.bind]; constructor
     intro y; apply ExtractNonDet.bind <;> solve_by_elim
 
-instance ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
+def ExtractNonDet.pure' : ExtractNonDet (Pure.pure (f := NonDetT m) x) := by
   dsimp [Pure.pure, NonDetT.pure]; constructor
 
-instance ExtractNonDet.liftM (x : m α) :
+def ExtractNonDet.liftM (x : m α) :
   ExtractNonDet (liftM (n := NonDetT m) x) := by
     dsimp [_root_.liftM, monadLift, MonadLift.monadLift]; constructor
     intro y; apply ExtractNonDet.pure'

tests/elab/5672.lean

@@ -20,7 +20,8 @@ Uses `def` variable inclusion rules
 -/
 section
 variable (x : Nat)
-instance b : A := by
+@[reducible]
+def b : A := by
   cases x <;> exact {}
 /-- info: b (x : Nat) : A -/
 #guard_msgs in #check b

tests/elab/impossibleInstance.lean

@@ -0,0 +1,22 @@
+class MyClass (α : Type u) where
+  point : α
+
+/--
+error: Instance @bad1 has arguments n : Nat that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type.
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+instance bad1 {α : Type} [Inhabited α] (n : Nat) : MyClass α := sorry
+
+/--
+error: Instance @bad2 has arguments n : Nat, m : Nat that are impossible to infer. Those arguments are not instance-implicit and do not appear in another instance-implicit argument or the return type.
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+instance bad2 {α : Type} [Inhabited α] (n m : Nat) : MyClass α := sorry
+
+/-- warning: declaration uses `sorry` -/
+#guard_msgs in
+instance good {α : Type} [Inhabited α] : MyClass α := sorry

tests/elab/isDefEqProjIssue.lean

@@ -77,10 +77,12 @@ class Foo where
   x : Nat
   y : Nat
 
-instance f (x : Nat) : Foo :=
+@[reducible]
+def f (x : Nat) : Foo :=
   { x, y := ack 10 10 }
 
-instance g (x : Nat) : Foo :=
+@[reducible]
+def g (x : Nat) : Foo :=
   { x, y := ack 10 11 }
 
 open Lean Meta

tests/elab/nonClassInstance.lean

@@ -0,0 +1,37 @@
+/-! Registering an instance whose target type is not a class should warn. -/
+
+structure Foo where
+  x : Nat
+
+class Bar where
+  x : Nat
+
+/-- error: instance `instFoo` target `Foo` is not a type class. -/
+#guard_msgs in
+instance instFoo : Foo := ⟨0⟩
+
+-- Applying @[instance] to a non-class def should also warn
+def instFoo2 : Foo := ⟨1⟩
+
+/-- error: instance `instFoo2` target `Foo` is not a type class. -/
+#guard_msgs in
+attribute [instance] instFoo2
+
+-- No warning for a proper class instance
+#guard_msgs in
+instance : Bar := ⟨0⟩
+
+-- No warning for a class instance with parameters
+class Baz (α : Type) where
+  x : α
+
+#guard_msgs in
+instance : Baz Nat := ⟨0⟩
+
+-- Warning for non-class with parameters
+structure Qux (α : Type) where
+  x : α
+
+/-- error: instance `instQux` target `Qux Nat` is not a type class. -/
+#guard_msgs in
+instance instQux : Qux Nat := ⟨0⟩

tests/elab/simp_proj_transparency_issue.lean

@@ -2,11 +2,11 @@ structure Foo where
   x : Nat
   y : Nat := 10
 
-@[instance]
+@[implicit_reducible]
 def f (x : Nat) : Foo :=
   { x := x + x }
 
-@[instance]
+@[implicit_reducible]
 def g (x : Nat) : Foo :=
   { x := x + x }
 

tests/elab/simp_proj_transparency_issue.lean.out.expected

@@ -1,2 +0,0 @@
-simp_proj_transparency_issue.lean:5:2-5:10: warning: instance `f` must be marked with `@[reducible]` or `@[implicit_reducible]`
-simp_proj_transparency_issue.lean:9:2-9:10: warning: instance `g` must be marked with `@[reducible]` or `@[implicit_reducible]`

tests/elab/test_simp_reducible_class.lean

@@ -17,7 +17,8 @@ namespace SimpReducibleClassField
 class X where
   x : Nat
 
-instance instX (n : Nat) : X where
+@[implicit_reducible]
+def instX (n : Nat) : X where
   x := n
 
 -- Test 1: plain simp, semireducible X.x (works on master)

tests/elab_fail/linterUnusedVariables.lean

@@ -154,7 +154,7 @@ class Baz (α : Type) where
     let y := 5
     3
 
-instance instBaz (α β : Type) : Baz α where
+@[reducible] def instBaz (α β : Type) : Baz α where
   baz (x : Nat) := 5
 
 

tests/elab_fail/linterUnusedVariables.lean.out.expected

@@ -52,7 +52,7 @@ Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:154:8-154:9: warning: unused variable `y`
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:157:20-157:21: warning: unused variable `β`
+linterUnusedVariables.lean:157:28-157:29: warning: unused variable `β`
 
 Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:158:7-158:8: warning: unused variable `x`