dangerous instance

Stream: general

[Kenny Lau]

import ring_theory.algebra_tower

instance is_algebra_tower.of_ring_hom {R A B : Type*}
  [comm_semiring R] [comm_semiring A] [comm_semiring B]
  [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
  @is_algebra_tower R A B _ _ _ _ (ring_hom.to_algebra f) _ :=
by { letI := (f : A →+* B).to_algebra,
exact is_algebra_tower.of_algebra_map_eq (λ x, (f.commutes x).symm) }

#lint

/-
/- Checking 1 declarations (plus 1 automatically generated ones) in the current file -/

/- The `instance_priority` linter reports: -/
/- DANGEROUS INSTANCE PRIORITIES.
The following instances always apply, and therefore should have a priority < 1000.
If you don't know what priority to choose, use priority 100.

If this is an automatically generated instance (using the keywords `class` and `extends`),
see note [lower instance priority] and see note [default priority] for instructions to change the priority: -/
#print is_algebra_tower.of_ring_hom /- set priority below 1000 -/
-/

[Kenny Lau]

why is this a dangerous instance?

[Kenny Lau]

given R-algebras A and B, and an R-alg hom f : A -> B, this is asserting that R, A, B form an algebra tower

[Kenny Lau]

where the structure of A-algebra on B is given by f

[Kenny Lau]

@Johan Commelin

[Reid Barton]

Johan is away for the next two weeks

[Kenny Lau]

oh

[Kenny Lau]

would you know why linter didn't like my instance?

[Reid Barton]

is (ring_hom.to_algebra f) appearing as a [] argument?

[Reid Barton]

that might be how the linter decides whether the instance matches on any variables

[Reid Barton]

only check () variables

[Reid Barton]

I'm just speculating though.

[Kenny Lau]

so is that a bug?

[Reid Barton]

Probably not, but it doesn't necessarily mean your instance is bad

[Sebastien Gouezel]

The linter does not say it is a bad instance, only that the priority should be lowered to 100 because this is an instance that always applies.

[Kenny Lau]

@Sebastien Gouezel but it doesn't always apply right

[Kenny Lau]

it's specifically for ring_hom.to_algebra

[Yury G. Kudryashov]

I think @Gabriel Ebner knows whether this instance is actually bad for lean.

[Mario Carneiro]

What are all the stub arguments in the instance?

[Mario Carneiro]

Looking at the linter source, it looks like @Reid Barton is correct. Any variables appearing in instance arguments are ignored for the purpose of determining if an instance "always applies"

[Mario Carneiro]

all arguments to is_algebra_tower are instance arguments except R A B

[Mario Carneiro]

I think it should be fine either way. You could either decrease the priority like it suggests, or @[nolint instance_priority]

[Mario Carneiro]

Although it is worth considering what you want to happen if this instance is competing with an instance for e.g. is_algebra_tower A (B x C) D

[Yury G. Kudryashov]

The question is whether Lean quickly decides that it can't apply this instance if [algebra] structure on B is not given by ring_hom.to_algebra _.

[Yury G. Kudryashov]

If yes, then this is a false positive of the linter.

[Kenny Lau]

Mario Carneiro said:

Although it is worth considering what you want to happen if this instance is competing with an instance for e.g. is_algebra_tower A (B x C) D

the point is that it will not, because then f would have to have type B \times C \ra[A] D

[Floris van Doorn]

Have you tried using this instance? Does Lean even apply it?

I'm worried that a typical case in which type-class inference for is_algebra_tower has to fire is when Lean knows the first 3 (explicit) arguments and doesn't know the last 6 (instance) arguments, so it needs to find an instance for @is_algebra_tower R A B ?m1 ?m2 ?m3 ?m4 ?m5 ?m6. In that case, this instance will happily unify, by setting ?m5 := ring_hom.to_algebra ?f. However, there is no way that ?f can be figured out by Lean.

I guess if Lean has to figure out something of the form @is_algebra_tower R A B ?m1 ?m2 ?m3 ?m4 (ring_hom.to_algebra f) ?m6, then this instance is useful, but I don't know when this actually happens (Lean infers type-class arguments from right to left, so how did it already know one of the type-class arguments?