[downstream PR] Julia's instance check

src/Init/Prelude.lean

@@ -1023,11 +1023,25 @@ theorem of_decide_eq_true [inst : Decidable p] : Eq (decide p) true → p := fun
   | isTrue  h₁ => h₁
   | isFalse h₁ => absurd h (Bool.ne_true_of_eq_false (decide_eq_false h₁))
 
+/--
+Variant of `of_decide_eq_true` that takes `Decidable` as an implicit argument, intended for
+forward reasoning.
+-/
+theorem of_decide_eq_true_forward {inst : Decidable p} : Eq (decide p) true → p :=
+  of_decide_eq_true
+
 theorem of_decide_eq_false [inst : Decidable p] : Eq (decide p) false → Not p := fun h =>
   match (generalizing := false) inst with
   | isTrue  h₁ => absurd h (Bool.ne_false_of_eq_true (decide_eq_true h₁))
   | isFalse h₁ => h₁
 
+/--
+Variant of `of_decide_eq_false` that takes `Decidable` as an implicit argument, intended for
+forward reasoning.
+-/
+theorem of_decide_eq_false_forward {inst : Decidable p} : Eq (decide p) false → Not p :=
+  of_decide_eq_false
+
 theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide (Eq a a)) true :=
   match (generalizing := false) inst a a with
   | isTrue  _  => rfl

src/Init/WF.lean

@@ -523,7 +523,7 @@ The `wfParam` gadget is used internally during the construction of recursive fun
 wellfounded recursion, to keep track of the parameter for which the automatic introduction
 of `List.attach` (or similar) is plausible.
 -/
-@[implicit_reducible] def wfParam {α : Sort u} (a : α) : α := a
+@[instance_reducible] def wfParam {α : Sort u} (a : α) : α := a
 
 /--
 Reverse direction of `dite_eq_ite`. Used by the well-founded definition preprocessor to extend the

src/Lean/Class.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Attributes
+public import Lean.ScopedEnvExtension
 import Lean.Util.CollectLevelParams
 public section
 namespace Lean
@@ -174,6 +175,48 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   let outLevelParams := computeOutLevelParams decl.type outParams decl.levelParams
   return classExtension.addEntry env { name := clsName, outParams, outLevelParams }
 
+/--
+Classes marked `@[lax_instance_defeq]` are exempt from the strict instance-argument discipline of
+`backward.isDefEq.respectTransparency.instances`: a value assigned to an instance metavariable of
+such a class is not required to have a type that matches the metavariable's type at `.instances`
+transparency. The instance-argument check of `simp`/`dsimp` (`dsimp.resynthInstances`) and the
+`linter.tacticCheckInstances` linter skip these classes as well.
+-/
+builtin_initialize laxInstanceDefeqExt : SimpleScopedEnvExtension Name NameSet ←
+  registerSimpleScopedEnvExtension {
+    initial  := {}
+    addEntry := fun s n => s.insert n
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `lax_instance_defeq
+    descr := "exempt instances of a class from the strict defeq check at `.instances` \
+      transparency (see `backward.isDefEq.respectTransparency.instances`)"
+    add   := fun declName stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless isClass (← getEnv) declName do
+        throwError "invalid `lax_instance_defeq`, `{.ofConstName declName}` is not a class"
+      laxInstanceDefeqExt.add declName kind
+  }
+
+/-- Whether a class type's result sort is `Prop`. -/
+private def isPropValued : Expr → Bool
+  | .forallE _ _ b _ => isPropValued b
+  | .sort u          => u == .zero
+  | _                => false
+
+/--
+Return `true` if instances of class `className` are exempt from the strict defeq check at
+`.instances` transparency: the class is marked `@[lax_instance_defeq]`, or it is propositional
+(proof irrelevance makes a stale instance argument harmless there). See `laxInstanceDefeqExt`.
+-/
+def isLaxInstanceDefeqClass (env : Environment) (className : Name) : Bool :=
+  (laxInstanceDefeqExt.getState env).contains className ||
+    match env.find? className with
+    | some info => isPropValued info.type
+    | none => false
+
 /--
 Registers an inductive type or structure as a type class. Using `class` or `class inductive` is
 generally preferred over using `@[class] structure` or `@[class] inductive` directly.

src/Lean/Elab/BuiltinTerm.lean

@@ -349,6 +349,42 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
   let args := mvars ++ args.drop mvars.size
   instantiateMVars (mkAppN fn args)
 
+/--
+Best-effort unification of the user-supplied `type` against the `expectedType` to resolve
+user-placed `_` placeholders. We decompose both sides as applications of a common head and
+unify arguments position-by-position, skipping instance-implicit positions.
+
+Instance-implicit arguments of `type` are fresh synthetic class metavariables introduced by
+`elabType` that will be discarded by `resynthInstImplicitArgs`. Routing them through `isDefEq`
+serves no purpose and can spuriously fail: assigning a synthetic class metavariable triggers
+a transparency cap at `.instances` in the type-equality check (see
+`backward.isDefEq.respectTransparency.instances`), which prevents non-`[reducible]` definitions
+from unfolding — so, e.g., `Neg (Nat ⧸ n) =?= Neg (Zmod n)` fails even though `Zmod` reduces
+to `Nat ⧸ n` at `.default` transparency. The outer `isDefEq` then fails and rolls back the
+useful assignments made to user `_` placeholders.
+
+When the two sides do not share a common-shape head, we fall back to a plain `isDefEq`.
+Per-argument `isDefEq` calls are best-effort: a failure at one position does not roll back
+successes at others.
+-/
+private def unifyTypeForInferInstanceAs (type expectedType : Expr) : TermElabM Unit := do
+  let typeFn := type.getAppFn
+  let expectedFn := expectedType.getAppFn
+  let typeArgs := type.getAppArgs
+  let expectedArgs := expectedType.getAppArgs
+  unless typeFn.isConst && expectedFn.isConst
+      && typeFn.constName! == expectedFn.constName!
+      && typeArgs.size == expectedArgs.size do
+    discard <| isDefEq type expectedType
+    return
+  unless (← isDefEq typeFn expectedFn) do
+    return
+  let (_, bis, _) ← forallMetaTelescope (← inferType typeFn)
+  for i in [:typeArgs.size] do
+    if i < bis.size && bis[i]!.isInstImplicit then
+      continue
+    discard <| isDefEq typeArgs[i]! expectedArgs[i]!
+
 @[builtin_term_elab Lean.Parser.Term.inferInstanceAs] def elabInferInstanceAs : TermElab := fun stx expectedType? => do
   -- The type argument is the last child (works for both `inferInstanceAs T` and `inferInstanceAs <| T`)
   let typeStx := stx[stx.getNumArgs - 1]!
@@ -363,7 +399,7 @@ private def resynthInstImplicitArgs (type : Expr) : TermElabM Expr := do
   let type ← withSynthesize do
     let type ← elabType typeStx
     -- Unify with expected type to resolve metavariables (e.g., `_` placeholders)
-    discard <| isDefEq type expectedType
+    unifyTypeForInferInstanceAs type expectedType
     return type
   -- Re-infer instance-implicit args, so that synthesis is not influenced by the expected type's
   -- instance choices.

src/Lean/Environment.lean

@@ -2327,7 +2327,8 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   let numPublicConsts := modules.foldl (init := 0) fun numPublicConsts mod => Id.run do
     if !mod.isExported then numPublicConsts else
       let some data := mod.publicModule? | numPublicConsts
-      numPublicConsts + data.constants.size
+      -- binop issue: can't synthesize `HAdd Nat Nat (Id Nat)`; solved using `pure`
+      pure <| numPublicConsts + data.constants.size
   let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numExtraConsts)
   let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts)
   let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts)

src/Lean/Linter/TacticTypeCheck.lean

@@ -17,16 +17,19 @@ open Lean Elab Command
 open Lean.Linter (logLint)
 
 /--
-Warn when the goal target is not type-correct at `.implicit` transparency.
-This can happen when e.g. `unfold` leaves hypotheses whose types still refer to
-the pre-unfolded definition, preventing `rw`/`simp` from matching patterns.
+Whether a `linter.tacticCheckInstances` warning has already been logged for this command, e.g. by
+`simp` checking its own intermediate results while the command was elaborated.
 -/
-register_builtin_option linter.tacticCheckInstances : Bool := {
-  defValue := false
-  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency"
-}
+private def alreadyReported : CommandElabM Bool := do
+  -- `Command.State.messages` is reset per command, but by the time linters run its messages have
+  -- been marked reported, which `MessageLog.toList` does not return.
+  return (← get).messages.reportedPlusUnreported.any
+    (·.data.hasTag (· == linter.tacticCheckInstances.name))
 
-/-- A linter that runs `Meta.check _ .implicit` on every tactic goal. -/
+/--
+A linter that runs `Meta.check _ .implicit` and `Meta.findInstanceArgMismatch?` on every tactic
+goal.
+-/
 def tacticCheckInstances : Linter where
   run _cmdStx := do
     -- Do *not* check `linter.all` here, this linter is purely for debugging
@@ -35,8 +38,10 @@ def tacticCheckInstances : Linter where
     let infoTrees := (← get).infoState.trees.toArray
     -- Once any tactic step in this command has produced a warning, suppress
     -- all further checks: a bad lctx typically persists across many tactic
-    -- steps
-    let warned : IO.Ref Bool ← IO.mkRef false
+    -- steps. `simp` runs the same instance-argument check on its intermediate
+    -- results during elaboration, so start out suppressed if it already
+    -- reported one.
+    let warned : IO.Ref Bool ← IO.mkRef (← alreadyReported)
     for tree in infoTrees do
       -- `postNode` so children are visited before parents: leaf tactic infos
       -- (the actual user-written `unfold`, `rw`, ...) fire before the
@@ -56,7 +61,8 @@ def tacticCheckInstances : Linter where
         -- `.implicit` check fails, the defs unfolded at `.default` but not at
         -- `.implicit` are the candidates for `@[implicit_reducible]` and get
         -- reported to the user. The pattern mirrors `mkUnfoldAxiomsNote` in
-        -- `Lean.Meta.Check`.
+        -- `Lean.Meta.Check`. If it succeeds, we look for instance arguments
+        -- that stop matching one transparency level down.
         -- `kind` selects the wording of the warning:
         --   * "initial" — the failure is in `goalsBefore` of the first tactic
         --     (i.e. the `by` block started with a bad goal).
@@ -74,30 +80,37 @@ def tacticCheckInstances : Linter where
             let counterDefault := (← get).diag.unfoldCounter
             -- Reset and try at `.implicit`.
             modify ({ · with diag := origDiag })
-            try
-              Meta.check target .implicit
+            let implicitError? : Option Exception ←
+              try Meta.check target .implicit; pure none catch e => pure (some e)
+            let some e := implicitError? | do
+              -- Type-correct at `.implicit`, but `simp`/`rw` unify instance-implicit arguments at
+              -- `.instances`, where an argument left behind by an earlier rewrite may no longer
+              -- match.
+              let some msg ← Meta.findInstanceArgMismatch? target | return none
+              return some m!"The {kind} tactic goal has an instance argument whose type does not \
+                match at `.instances` transparency. `simp` and `rw` unify instance-implicit \
+                arguments at that transparency. Lemmas that mention this instance do not \
+                apply:{indentD msg}"
+            let counterInst := (← get).diag.unfoldCounter
+            let diff := Meta.subCounters counterDefault counterInst
+            let env ← getEnv
+            let candidates : List MessageData :=
+              diff.toList.filterMap fun (n, count) => do
+                guard <| count > 0
+                guard <| getReducibilityStatusCore env n matches .semireducible
+                guard <| !Meta.isInstanceCore env n
+                return m!"{.ofConstName n}"
+            if candidates.isEmpty then
               return none
-            catch e =>
-              let counterInst := (← get).diag.unfoldCounter
-              let diff := Meta.subCounters counterDefault counterInst
-              let env ← getEnv
-              let candidates : List MessageData :=
-                diff.toList.filterMap fun (n, count) => do
-                  guard <| count > 0
-                  guard <| getReducibilityStatusCore env n matches .semireducible
-                  guard <| !Meta.isInstanceCore env n
-                  return m!"{.ofConstName n}"
-              if candidates.isEmpty then
-                return none
-              let remedy : MessageData := match kind with
-                | "initial" => "consider rephrasing the goal or marking"
-                | _         => "consider using propositional rewriting or marking"
-              return some m!"{kind} tactic goal is not type-correct at \
-                `.implicit` transparency; {remedy} some of the following as \
-                `@[implicit_reducible]`:\
-                {indentD (.joinSep candidates Format.line)}\n\
-                Full error:\
-                {indentD e.toMessageData}"
+            let remedy : MessageData := match kind with
+              | "initial" => "consider rephrasing the goal or marking"
+              | _         => "consider using propositional rewriting or marking"
+            return some m!"{kind} tactic goal is not type-correct at \
+              `.implicit` transparency; {remedy} some of the following as \
+              `@[implicit_reducible]`:\
+              {indentD (.joinSep candidates Format.line)}\n\
+              Full error:\
+              {indentD e.toMessageData}"
           -- Always restore the original diagnostics snapshot.
           modify ({ · with diag := origDiag })
           return result

src/Lean/Meta/Check.lean

@@ -17,6 +17,28 @@ This is not the Kernel type checker, but an auxiliary method for checking
 whether terms produced by tactics and `isDefEq` are type correct.
 -/
 
+namespace Lean.Linter
+
+/--
+Warn when the goal target is not type-correct at `.implicit` transparency, or when it contains an
+instance argument that only has the expected type above `.instances` transparency.
+
+The former happens when e.g. `unfold` leaves hypotheses whose types still refer to the pre-unfolded
+definition, preventing `rw`/`simp` from matching patterns. The latter happens when e.g. an `rfl`
+lemma rewrites a value without updating the instances mentioning it, preventing `rw`/`simp` from
+unifying the instance argument.
+
+The option lives here rather than next to the linter in `Lean.Linter.TacticTypeCheck` because
+`simp` reads it too, to run `findInstanceArgMismatch?` on its intermediate results.
+-/
+register_builtin_option linter.tacticCheckInstances : Bool := {
+  defValue := false
+  descr := "enable the linter that type-checks every tactic goal at `.implicit` transparency and \
+    checks its instance arguments at `.instances` transparency"
+}
+
+end Lean.Linter
+
 namespace Lean.Meta
 
 private def ensureType (e : Expr) : MetaM Unit := do
@@ -337,6 +359,65 @@ def check (e : Expr) (transparency : TransparencyMode := .all) : MetaM Unit :=
       trace[Meta.check] ex.toMessageData
       throw ex
 
+/--
+Describes the first application in `e` whose instance-implicit argument has the expected type at
+`.implicit` transparency but not at `.instances`, if there is one.
+
+`check e .implicit` accepts such an application, but `simp` and `rw` unify instance-implicit
+arguments at `.instances`, so a lemma mentioning the instance still fails to apply. This state
+typically arises when an `rfl` lemma rewrites a value without updating the instances mentioning it.
+-/
+partial def findInstanceArgMismatch? (e : Expr) : MetaM (Option MessageData) :=
+  withDefault <| visit e |>.run
+where
+  visit (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    checkCache { val := e : ExprStructEq } fun _ => do
+      match e with
+      | .forallE ..      => visitForall e
+      | .lam ..          => visitLambdaLet e
+      | .letE ..         => visitLambdaLet e
+      | .app f a         =>
+        if let some msg ← visit f then return some msg
+        if let some msg ← visit a then return some msg
+        visitApp f a
+      | .mdata _ e       => visit e
+      | .proj _ _ e      => visit e
+      | _                => return none
+
+  visitApp (f a : Expr) : MetaM (Option MessageData) := do
+    let (expectedType, binfo) ← try getFunctionDomain f catch _ => return none
+    unless binfo.isInstImplicit do return none
+    if let some className ← isClass? expectedType then
+      if isLaxInstanceDefeqClass (← getEnv) className then return none
+    let aType ← try inferType a catch _ => return none
+    let defEqAt (transparency : TransparencyMode) : MetaM Bool :=
+      withoutModifyingState <| withTransparency transparency <| isDefEqGuarded expectedType aType
+    if (← defEqAt .instances) then return none
+    -- A mismatch that persists at `.implicit` is an outright type error, which `check e .implicit`
+    -- reports with more context.
+    unless (← defEqAt .implicit) do return none
+    let app := (mkApp f a).setAppPPExplicit
+    addMessageContext m!"The instance argument{indentExpr a}\n\
+      {← mkHasTypeButIsExpectedMsg aType expectedType
+        (trailing? := m!"in the application{indentExpr app}") (trailingExprs := #[app])}"
+
+  visitLambdaLet (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    lambdaLetTelescope e fun xs b => do
+      for x in xs do
+        match ← getFVarLocalDecl x with
+        | .cdecl (type := t) .. =>
+          if let some msg ← visit t then return some msg
+        | .ldecl (type := t) (value := v) .. =>
+          if let some msg ← visit t then return some msg
+          if let some msg ← visit v then return some msg
+      visit b
+
+  visitForall (e : Expr) : MonadCacheT ExprStructEq (Option MessageData) MetaM (Option MessageData) :=
+    forallTelescope e fun xs b => do
+      for x in xs do
+        if let some msg ← visit (← getFVarLocalDecl x).type then return some msg
+      visit b
+
 /--
 Runs `x` and, on any error, lazily checks whether `e` is type-correct at `instances` transparency.
 If not, appends an explanatory note to the error message.