AlgHom to RingHom coercion is bad

Stream: mathlib4

[Kenny Lau]

import Mathlib

def foo : ℝ →ₐ[ℤ] ℚ := sorry
#check (foo : _ →+* _) -- fails
#check (foo : ℝ →+* ℚ) -- works

(I think I can potentially minimise the import Mathlib away edit: i tried and failed)
so basically I think this fails because Lean doesn't know which base ring for the algebra to try?

[Kenny Lau]

Then the problem this creates is that I would manually type in foo.toRingHom and then the simp linter and co. wouldn't like this

[Edward van de Meent]

looking at the trace, for whatever reason typeclass instance synthesis complains it can't find FunLike (ℝ →ₐ[ℤ] ℚ) ?_ ?_ (even though #synth succeeds for this?)

[Kenny Lau]

Actually it has nothing to do with the extra variable, even RingEquiv to RingHom is bad:

import Mathlib

def foo : ℝ ≃+* ℚ := sorry
#check (foo : _ →+* _) -- fails
#check (foo : ℝ →+* ℚ) -- works

[Kenny Lau]

the entire chain of coercion in this tree is basically unusable

[Edward van de Meent]

if you use set_option trace.Meta.synthInstance true, you'll see that indeed it finds the coersion induced by the RingHomClass instance for AlgHom and RingEquiv respectively, but fails to apply the appropriate FunLike or EquivLike instance

[Edward van de Meent]

i.e. we get trace like this:

[tryResolve] 💥️ EquivLike (ℝ ≃+* ℚ) ?m.50 ?m.51 ≟ EquivLike (?m.1154 ≃+* ?m.1155) ?m.1154 ?m.1155

[Edward van de Meent]

which seems like it should unify

[Edward van de Meent]

looking at the universes of these, maybe there's some issue there? the lhs Equivlike lives in the simple Type (max ?u.49 ?u.48), while the rhs lives in the more complicated Type (max (max (max 0 ?u.1153 ?u.1152) ?u.1152) ?u.1153) for whatever reason

[Edward van de Meent]

maybe the issue is that lean can't figure out what values the universe levels should have, and so just shuts down completely?

[Edward van de Meent]

(i'm not at all familiar with the precise specs of unification, i'm just pointing at things which look weird)

[Kenny Lau]

hmm, do you know anyone who might know about this?

[Edward van de Meent]

i have the suspicion that Anne Baanen knows a lot about these design decisions and instance inference subtleties, but they might be very busy with other things... i think if we wait someone else might provide insight

[Edward van de Meent]

(and from the top of my head i don't know who else i would ask)

[Michael Stoll]

Here is an excerpt of a more detailed trace:

        [isDefEq] [0.000447] 💥️ EquivLike (ℝ ≃+* ℚ) ?m.50 ?m.51 =?= EquivLike (?m.536 ≃+* ?m.537) ?m.536 ?m.537 ▼
          [] [0.000357] ✅️ ℝ ≃+* ℚ =?= ?m.536 ≃+* ?m.537 ▼
            [] [0.000026] ✅️ ℝ =?= ?m.536 ▶
            [] [0.000017] ✅️ ℚ =?= ?m.537 ▶
            [] [0.000055] ✅️ Real.instMul =?= ?m.538 ▶
            [] [0.000041] ✅️ Rat.instMul =?= ?m.539 ▶
            [] [0.000053] ✅️ Real.instAdd =?= ?m.540 ▶
            [] [0.000067] ✅️ Rat.instAdd =?= ?m.541 ▶
          [] [0.000006] 💥️ ?m.50 =?= ℝ ▼
            [] ?m.50 [nonassignable] =?= ℝ [nonassignable]

The problem seems to be that the metavariable here is "nonassignable", causing the unification to fail. I'm not sure where this comes from, but it may have some relation to lean4#8364 (where something similar happens with an explicit coercion arrow).

[Edward van de Meent]

how did you get that detailed trace? is there some option?

[Michael Stoll]

import Mathlib

set_option trace.Meta.synthInstance true
set_option trace.Meta.isDefEq true
set_option trace.profiler true

def foo : ℝ ≃+* ℚ := sorry
#check (foo : _ →+* _) -- fails

[Kenny Lau]

push... do other people dealing with ring homs and ring equivs have the same issue?

[Kevin Buzzard]

yeah, I just put .toRingHom

[Kenny Lau]

yes, and then the simp linter complains that you haven't put it in simp normal form

[Kevin Buzzard]

Oh well then just add the source and target types?

[Kenny Lau]

then the statement becomes bigger

[Kevin Buzzard]

is the logic one of these silly "yes I know you want to coerce ℝ ≃+* ℚ to X →+* Y but my typeclass inference system is so flexible that as far as I know X and Y can be anything so I'll just give up now"?

[Kenny Lau]

well Michael Stoll tried to read the trace and reached a "nonassignable" metavariable but i have no idea what any of those mean

[Andrew Yang]

Kenny Lau said:

yes, and then the simp linter complains that you haven't put it in simp normal form

You use RingHomClass.toRingHom instead. But people seem to be phasing this out.

[Anne Baanen]

Michael Stoll said:

Here is an excerpt of a more detailed trace:

        [isDefEq] [0.000447] 💥️ EquivLike (ℝ ≃+* ℚ) ?m.50 ?m.51 =?= EquivLike (?m.536 ≃+* ?m.537) ?m.536 ?m.537 ▼
          [] [0.000357] ✅️ ℝ ≃+* ℚ =?= ?m.536 ≃+* ?m.537 ▼
            [] [0.000026] ✅️ ℝ =?= ?m.536 ▶
            [] [0.000017] ✅️ ℚ =?= ?m.537 ▶
            [] [0.000055] ✅️ Real.instMul =?= ?m.538 ▶
            [] [0.000041] ✅️ Rat.instMul =?= ?m.539 ▶
            [] [0.000053] ✅️ Real.instAdd =?= ?m.540 ▶
            [] [0.000067] ✅️ Rat.instAdd =?= ?m.541 ▶
          [] [0.000006] 💥️ ?m.50 =?= ℝ ▼
            [] ?m.50 [nonassignable] =?= ℝ [nonassignable]

The problem seems to be that the metavariable here is "nonassignable", causing the unification to fail. I'm not sure where this comes from, but it may have some relation to lean4#8364 (where something similar happens with an explicit coercion arrow).

I believe what happens is that ?m.50 is the metavariable created by the underscores in _ →+* _. Then a new context is created at some point in the search for a coercion, and metavariables outside of that context become nonassignable. The motivation for this is that you wouldn't want (↑x : _), where the expected type is unknown, to commit to the first coercion it finds, if later on the expected type is figured out.

[Anne Baanen]

Of course, here the resulting type is in fact determined by the incoming type, but that is not the case for every coercion.

[Anne Baanen]

Would it be an idea to have a fun_coe% elaborator that picks the right coercion here?

[Matthew Ballard]

You enter a unification step for a FunLike instance which bumps the meta context up by one and then you want to assign the original metavariable from the _ which is now at the wrong depth to do this.

[Kenny Lau]

Andrew Yang said:

Kenny Lau said:

yes, and then the simp linter complains that you haven't put it in simp normal form

You use RingHomClass.toRingHom instead. But people seem to be phasing this out.

well i'm afraid this might be the best option for now, thanks for teaching me this; what do you mean by people phasing this out?

[Matthew Ballard]

Although here all meta variables at the new depth are already assigned…