apply_instance and reducibility flag

[sgouezel]

apply_instance fails to find an instance, although it finds one for another problem which is defeq to the first one, even with the flag tactic.transparency.instances. MWE, based on mathlib:

import analysis.normed_space.basic

section normed_module
set_option default_priority 100 -- see Note [default priority]
class normed_module (α : Type*) (β : Type*) [normed_ring α] [normed_group β]
  extends semimodule α β :=
(norm_smul_le : ∀ (a:α) (b:β), ∥a • b∥ ≤ ∥a∥ * ∥b∥)
end normed_module

variables {𝕜 : Type}  {n : ℕ} {E : fin n → Type}
[A : normed_field 𝕜] [N : ∀i, normed_group (E i)] [∀i, normed_module 𝕜 (E i)]

-- Two different ways to say: Π (i : fin n), module 𝕜 (E i)

set_option trace.class_instances true

lemma all_right :
Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance

lemma fails :
Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A)))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance -- fails
-- all_right  -- works

The two terms in the two lemmas are defeq with tactic.transparency.instances, and the subterms are also defeq with tactic.transparency.instances, but they are not defeq with tactic.transparency.reducible, as shown by the following:

lemma outer_works_with_transparency.instances :
  (Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)))
   =
  Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A)))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by tactic.reflexivity tactic.transparency.instances -- works

lemma inner_works_with_transparency.instances :
  (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
  =
  (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.instances --works

lemma inner_fails_with_transparency.reducible :
  (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
  =
  (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.reducible -- fails

Mario's guess on Zulip is that apply_instance probably passes the wrong flag to subproblems (see discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197786186)

Tested on Lean 3.11 and 3.13.1

(Example edited for 3.16.0)

[gebner]

I'm pretty sure this is a unification problem and not a transparency issue. During type class search we need to unify the instance with the goal, this is much harder than checking definitional equality of terms without metavariables.

[sgouezel]

I just stumbled on the same issue (with pretty complicated pi types, again). Is there hope that https://github.com/leanprover-community/lean/pull/300 could change something here? (It involves pi types and instance search and reducibility flags, so from a distance it sounds similar, but the details look rather different).

[sgouezel]

Just checked on Lean 3.16, and the behavior is the same. I guess you're right, this is a (complicated) unification problem.