structure construction hangs forever

Stream: mathlib4

[Sébastien Gouëzel]

In the following structure construction, if I sorry out any of the Prop fields then the definition works fine, but when I unsorry everything it hangs forever. Any idea of what might be going on, and how to fix it?

import Mathlib

noncomputable def RCLike.copy_Algebra {𝕜 : Type*} (h : RCLike 𝕜)  (hk : NormedField 𝕜)
    (h'' : hk = h.toNormedField) : @Algebra ℝ 𝕜 _ (@Ring.toSemiring 𝕜
    (@SeminormedRing.toRing 𝕜
      (@SeminormedCommRing.toSeminormedRing 𝕜
        (@NormedCommRing.toSeminormedCommRing 𝕜
          (@NormedField.toNormedCommRing 𝕜 hk))))) :=
  { smul := (@Algebra.toSMul _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)).smul
    toFun := @Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)
    map_one' := by
      let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
      convert @OneHom.map_one' _ _ _ (_) (@MonoidHom.toOneHom _ _ _ (_)
        (@RingHom.toMonoidHom _ _ _ (_) Z))
    map_mul' := by
      intro x y
      let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
      convert @MulHom.map_mul' _ _ _ (_) (@MonoidHom.toMulHom _ _ _ (_)
        (@RingHom.toMonoidHom _ _ _ (_) Z)) x y
    map_zero' := by
      let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
      convert @ZeroHom.map_zero' _ _ _ (_) (@AddMonoidHom.toZeroHom _ _ _ (_)
        (@RingHom.toAddMonoidHom _ _ _ (_) Z))
    map_add' := by
      intro x y
      let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
      convert @AddHom.map_add' _ _ _ (_) (@AddMonoidHom.toAddHom _ _ _ (_)
        (@RingHom.toAddMonoidHom _ _ _ (_) Z)) x y
    commutes' := by
      intro r x
      convert @Algebra.commutes' _ _ _ (_)
        (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra) r x
    smul_def' := by
      intro r x
      convert @Algebra.smul_def' _ _ _ (_)
        (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra) r x }

[Eric Wieser]

(this construction looks like a bad idea to me, but of course that's no reason for it to hang forever)

[Eric Wieser]

This spelling works:

import Mathlib

noncomputable def RCLike.copy_Algebra {𝕜 : Type*} (h : RCLike 𝕜)  (hk : NormedField 𝕜)
    (h'' : hk = h.toNormedField) : @Algebra ℝ 𝕜 _ (@Ring.toSemiring 𝕜
    (@SeminormedRing.toRing 𝕜
      (@SeminormedCommRing.toSeminormedRing 𝕜
        (@NormedCommRing.toSeminormedCommRing 𝕜
          (@NormedField.toNormedCommRing 𝕜 hk))))) :=
  { smul := (@Algebra.toSMul _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)).smul
    toFun := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
    map_one' := by subst h''; exact map_one _
    map_mul' := by subst h''; exact map_mul _
    map_zero' := by subst h''; exact map_zero _
    map_add' := by subst h''; exact map_add _
    commutes' := by subst h''; exact Algebra.commutes
    smul_def' := by subst h''; exact Algebra.smul_def }

[Kevin Buzzard]

I posted a question just like this a few months ago -- a problem that a student had. Presumably it's not fixed with suppress_compilation? In the end I just factored out the proofs and for some reason it fixed it

[Eric Wieser]

I think suppress_compilation just means "add noncomputable to everything", so it would make no difference here

[Sébastien Gouëzel]

I had already tried with suppress_compilation, or fixing the universe, to no avail. The subst spelling works great, thanks a lot @Eric Wieser (although it would probably be better to understand what is going on and fix it, but I have no idea there).

[Julian Berman]

You don't happen to be on a 4.12 build by any chance? (On the last office hours Johan was debugging some slightly similar case I think in the sense that it was some definition that took really long but was faster if you sorried one of the fields -- but I think that was on 4.12 and not 4.11)

[Kevin Buzzard]

Here was my similar (but possibly not the same) problem. Same symptoms though -- sorrying a field made things quick, filling in all sorries made it extremely slow

[Kevin Buzzard]

PS your construction, like mine, doesn't hang forever -- you just have to be patient :-)