invalid parametric local instance errors on typeclass arguments

[kim-em]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

We check for parametric local instances, where the parameters are not inferrable, and reject these. However we could/should allow typeclass arguments.

Steps to Reproduce

class P (n : Nat)
class Q (n : Nat)
variable [∀ (n : Nat) [P n], Q n]
example [P 7] : Q 7 := inferInstance

Expected behavior:

This should just work.

This is a regression from Lean 3 behaviour, where

class P (n : nat)
class Q (n : nat)
variable [∀ (n : nat) [P n], Q n]
example [P 7] : Q 7 := by apply_instance

works fine.

Actual behavior:

invalid parametric local instance, parameter with type
  P n
does not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter.

Discussion

This is a useful and I think valid construction. We are only just running into this issue in the mathlib port at leanprover-community/mathlib4#5088, where we want to use

variable [∀ ⦃A B⦄ (f g : A ⟶ B) [IsReflexivePair f g], PreservesColimit (parallelPair f g) G]

It is possible to work around by defining new auxiliary typeclasses, but it would be nice to just support directly.

It is quite easy to fix: in checkLocalInstanceParameters, just replace if !b.hasLooseBVar 0 then with if bi != .instImplicit && !b.hasLooseBVar 0 then.

Versions

nightly-2023-07-06

[kim-em]

@gebner has suggested on zulip that this was intended behaviour, but I hope we can allow this.

It would be helpful to know whether this change might be made in Lean 4, so we can decide whether to wait for it in leanprover-community/mathlib4#5088 (one of the last remaining porting PRs!), or start implementing workarounds there.