fix: `grind` pattern validation
This PR fixes the `grind` pattern validator. It covers the case where
an instance is not tagged with the implicit instance binder. This
happens in declarations such as
```lean
ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
[self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
```
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 29e38c7..5736432 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -662,10 +662,23 @@
if pinfos[idx].hasFwdDeps then return .typeFormer else return .relevant
else
return .typeFormer
- else if (← x.fvarId!.getDecl).binderInfo matches .instImplicit then
- return .instImplicit
else
- return .relevant
+ let xDecl ← x.fvarId!.getDecl
+ if xDecl.binderInfo matches .instImplicit then
+ return .instImplicit
+ /-
+ **Note**: Even if the binder is not marked as instance implicit, we may still
+ synthesize it using type class resolution. The motivation is declarations such as
+ ```
+ ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
+ [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
+ ```
+ Recall that a similar approach is used in `simp`.
+ -/
+ else if (← isClass? xDecl.type).isSome then
+ return .instImplicit
+ else
+ return .relevant
private def getPatternFn? (pattern : Expr) (inSupport : Bool) (root : Bool) (argKind : PatternArgKind) : M (Option Expr) := do
if !pattern.isApp && !pattern.isConst then
@@ -860,27 +873,34 @@
for x in xs do
let fvarId := x.fvarId!
unless processed.contains fvarId do
- let xType ← inferType x
+ let xDecl ← fvarId.getDecl
+ let xType := xDecl.type
if fvarsFound.contains fvarId then
-- Collect free vars in `x`s type and mark as processed
fvarsFound := update fvarsFound xType
processed := processed.insert fvarId
modified := true
- else if (← fvarId.getDecl).binderInfo matches .instImplicit then
- -- If `x` is instance implicit, check whether
- -- we have found all free variables needed to synthesize instance
- if (← canBeSynthesized thmVars fvarsFound xType) then
- fvarsFound := fvarsFound.insert fvarId
- fvarsFound := update fvarsFound xType
- processed := processed.insert fvarId
- modified := true
- else if (← isProp xType) then
- -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
- -- add it to `fvarsFound` and mark it as processed.
- if checkTypeFVars thmVars fvarsFound xType then
- fvarsFound := fvarsFound.insert fvarId
- processed := processed.insert fvarId
- modified := true
+ else
+ /- **Note**: See comment at `getPatternArgKinds` -/
+ let instImplicit ← if xDecl.binderInfo matches .instImplicit then
+ pure true
+ else
+ pure <| (← isClass? xType).isSome
+ if instImplicit then
+ -- If `x` is instance implicit, check whether
+ -- we have found all free variables needed to synthesize instance
+ if (← canBeSynthesized thmVars fvarsFound xType) then
+ fvarsFound := fvarsFound.insert fvarId
+ fvarsFound := update fvarsFound xType
+ processed := processed.insert fvarId
+ modified := true
+ else if (← isProp xType) then
+ -- If `x` is a proposition, and all theorem variables in `x`s type have already been found
+ -- add it to `fvarsFound` and mark it as processed.
+ if checkTypeFVars thmVars fvarsFound xType then
+ fvarsFound := fvarsFound.insert fvarId
+ processed := processed.insert fvarId
+ modified := true
if fvarsFound.size == numParams then
return .ok
if !modified then
diff --git a/tests/lean/run/grind_pattern_validation_instance.lean b/tests/lean/run/grind_pattern_validation_instance.lean
new file mode 100644
index 0000000..a78519d
--- /dev/null
+++ b/tests/lean/run/grind_pattern_validation_instance.lean
@@ -0,0 +1,58 @@
+/-!
+Test for `grind` pattern validation. It covers the case where
+an instance is not tagged with the implicit instance binder.
+This happens in declarations such as
+```lean
+ZeroMemClass.zero_mem {S : Type} {M : outParam Type} {inst1 : Zero M} {inst2 : SetLike S M}
+ [self : @ZeroMemClass S M inst1 inst2] (s : S) : 0 ∈ s
+```
+-/
+
+def Set (α : Type u) := α → Prop
+
+/-- Membership in a set -/
+protected def Set.Mem (s : Set α) (a : α) : Prop :=
+ s a
+
+instance : Membership α (Set α) :=
+ ⟨Set.Mem⟩
+
+class SetLike (A : Type) (B : outParam Type) where
+ protected coe : A → Set B
+ protected coe_injective : Function.Injective coe
+
+instance [SetLike A B]: CoeTC A (Set B) where coe := SetLike.coe
+
+instance [SetLike A B] : Membership B A :=
+ ⟨fun p x => x ∈ (p : Set B)⟩
+
+class ZeroMemClass (S : Type) (M : outParam Type) [Zero M] [SetLike S M] : Prop where
+ zero_mem : ∀ s : S, (0 : M) ∈ s
+
+class Ring (R : Type) extends Zero R
+
+@[ext]
+structure Subring (M : Type) [Ring M] where
+ carrier : Set M
+ zero_mem' : 0 ∈ carrier
+
+instance {M} [Ring M] : SetLike (Subring M) M where
+ coe := Subring.carrier
+ coe_injective a b h := by ext; assumption
+
+theorem Subring.zero_mem {M} [Ring M] (s : Subring M) : 0 ∈ s :=
+ s.zero_mem'
+
+grind_pattern ZeroMemClass.zero_mem => 0 ∈ s
+
+instance {M} [Ring M] : ZeroMemClass (Subring M) M where
+ zero_mem := Subring.zero_mem
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+ grind
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+ grind only [ZeroMemClass.zero_mem]
+
+example {R : Type} [Ring R] (S : Subring R) : 0 ∈ S := by
+ grind only [Subring.zero_mem]
