IR failure in example

Stream: mathlib4

[Matthew Ballard]

Kevin Buzzard said:

What the heck is going on here BTW? I have an obscure error:

import Mathlib.GroupTheory.QuotientGroup
import Mathlib.Algebra.Hom.Equiv.TypeTags

open Subgroup

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) where
  conj_mem := Normal.conj_mem (H := S) inferInstance

def foo {G} [Group G] (S : Subgroup G) [Normal S] :
    Additive G ⧸ toAddSubgroup S ≃+ Additive (G ⧸ S) :=
  (QuotientAddGroup.quotientAddEquivOfEq sorry : Additive G ⧸ toAddSubgroup S ≃+ Additive G ⧸ _).trans
  (QuotientAddGroup.quotientKerEquivOfSurjective
    (MonoidHom.toAdditive (QuotientGroup.mk' S) : Additive G →+ Additive (G ⧸ S)) sorry)
/-
IR check failed at 'foo._rarg', error: unknown declaration 'QuotientAddGroup.quotientKerEquivOfSurjective'
-/

#check QuotientAddGroup.quotientKerEquivOfSurjective -- works fine

Edit: fixed by marking foo noncomputable. That's a pretty weird way to tell me to do that :-/

Did we diagnose failure in IR here?

[Kevin Buzzard]

I fixed it by searching for IR check.failed and discovering that they had shown up several times on Zulip and were always fixed by making the declaration noncomputable.

[Matthew Ballard]

Doesn't that just turn off the code generation?

[Gabriel Ebner]

Yes, this means that quotientKerEquivOfSurjective was not compiled (e.g. because it's marked noncomputable).

[Gabriel Ebner]

For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

[Gabriel Ebner]

Right now there's a lot of definitions unnecessarily marked noncomputable. This will change after !4#4097.

[Matthew Ballard]

Ok. I just ran into another incident. It turned out not be important for progress. Should I record it?

[Eric Wieser]

Gabriel Ebner said:

Right now there's a lot of definitions unnecessarily marked noncomputable. This will change after !4#4097.

Will it? IIRC Lean 4 doesn't complain if you marked something noncomputable that was actually computable.

[Gabriel Ebner]

It will change in the sense that !4#4097 removes countless noncomputable markers, as well as the reason why those were added in the first place (missing code for .rec).