Coercions in Mathlib4 vs Mathlib3

Stream: mathlib4

[Oliver Nash]

Looking at the porting PR https://github.com/leanprover-community/mathlib4/pull/2262 opened by @Lukas Miaskiwskyi I see some surprising (to me) warnings from the dangerousInstance linter.

It looks like in Mathlib4 an instance of Coe A B is "dangerous" if B drops some carrier types that were present in A. I'll illustrate this slightly vague statement with the following pair of MWEs.

[Oliver Nash]

First the Lean 3 version:

import tactic.default

variables (X Y : Type*)

class foo := (x : X)

structure bar [foo X] :=
(to_fun : X → X)
(to_fun_x : to_fun foo.x = foo.x)

structure baz [foo X] [foo Y] extends bar X :=
(to_fun' : X → Y)
(to_fun'_x : to_fun' foo.x = foo.x)

instance [foo X] [foo Y] : has_coe (baz X Y) (bar X) := ⟨baz.to_bar⟩

[Oliver Nash]

Now the Lean 4 version:

import Mathlib.Logic.Basic

variable (X Y : Type _)

class Foo := (x : X)

structure Bar [Foo X] :=
(to_fun : X → X)
(to_fun_x : to_fun Foo.x = Foo.x)

structure Baz [Foo X] [Foo Y] extends Bar X :=
(to_fun' : X → Y)
(to_fun'_x : to_fun' Foo.x = Foo.x)

-- Should I drop this or use `CoeOut` instead?
instance [Foo X] [Foo Y] : Coe (Baz X Y) (Bar X) := ⟨Baz.toBar⟩

[Oliver Nash]

They both typecheck but the Lean 4 version gets a warning from the linter than the Lean 3 version does not. Specifically:

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check instCoeBazBar /- generates subgoals with metavariables: argument 4 inst✝ : Foo ?Y -/

[Oliver Nash]

I looked at the places where I would have expected this to come up already in Mathlib4 but all the examples I found (e.g., coercion of linear maps to additive monoid homs) achieve their coercion using @Anne Baanen 's morphisms-as-typeclasses-design (e.g., using semilinear_map_class and add_monoid_hom_class) so the issue does not arise.

[Oliver Nash]

So what is the right thing to do in a situation like the one I have outlined above. What should be the Lean 4 equivalent of this Lean 3 statement: https://github.com/leanprover-community/mathlib/blob/bd9851ca476957ea4549eb19b40e7b5ade9428cc/src/algebra/lie/basic.lean#L482

[Oliver Nash]

Maybe just CoeOut instead of Coe?

[James Gallicchio]

in the case of your MWE I think you'd expect Foo X/Foo Y to always be solved by unification rather than tc inference, so you'd mark them implicit in the instance instead

instance {FX : Foo X} {FY : Foo Y} : Coe (Baz X Y) (Bar X) := sorry

[James Gallicchio]

in the mathlib case, you probably can do the same, but there are so many variables floating around in context that it might be a pain to reintroduce them all >_<

[Oliver Nash]

The linter still emits a dangerousInstance warning to me if I make the typeclass variables implicit as you suggest (and it another linter also incorrectly complains that FX and FY are unused).

[Oliver Nash]

As well as knowing how I should fix this, I'd like to understand what has been changed about coercions and why (provided it's not a rabbit hole).

[Oliver Nash]

Aha, in very recently merged code here I see this:

instance coeOutRingHom : CoeOut (A →ₐ[R] B) (A →+* B) :=
  ⟨AlgHom.toRingHom⟩
#align alg_hom.coe_ring_hom AlgHom.coeOutRingHom

Which suggests that at least one other person thought the right thing to do was just to use CoeOut instead of Coe. Maybe @Pol'tta / Kô Miyahara can comment?

[Gabriel Ebner]

Yeah, CoeOut is the way to go here.

[Oliver Nash]

Thanks!

[Pol'tta / Miyahara Kō]

I used CoeOut in these instances to avoid dangerousInstance linter.

[Yuyang Zhao]

I was confused about the use of CoeOut in mathlib4 for a long time. Docstr says that use CoeOut α β if the variables in the type α are a superset of the variables in β, but there are fewer AlgHoms than RingHoms. Also we used Coe in MonoidHom.coeToMulHom MonoidHom.coeToOneHom etc. I would like to know if there is a reason to use CoeOut here.

[Yuyang Zhao]

Mario Carneiro said:

you would need something like CoeHead? CoeOut* CoeIn* CoeTail? where CoeOut : A -> outParam B and CoeIn : outParam A -> B

Ah I see. So for homomorphisms (or other FunLike things), it's the opposite of the corresponding type, is it?

[Gabriel Ebner]

but there are fewer AlgHoms than RingHoms.

It's not about the cardinality of the set of homomorphisms, it's about number of variables in the Lean type! A →ₐ[R] B has a variable R that does not appear in A →* B, that's what the docstring refers to.