algebraic_closure makes Lean hang

Stream: general

[Chris Hughes]

This gives me excessive memory consumption errors. Any tips about what to do?

import field_theory.algebraic_closure

def examle {K : Type} [field K] : K ≃+* algebraic_closure K := sorry

[Alex J. Best]

Does it work if you fill in the def? I see the same behaviour with:

def a {K : Type} [field K] : algebraic_closure K ≃+* algebraic_closure K := sorry -- hangs
def b {K : Type} [field K] : algebraic_closure K ≃+* algebraic_closure K := ring_equiv.refl _ --works

[Eric Rodriguez]

Yeah, I think this is the "standard" lemma/def issue. I tend to make these sorts of defns a lemma until its done, and then change then to def at the end

[Eric Rodriguez]

Iirc it's related to defs being able to change the 'actual' type depending on the contents

[Reid Barton]

What is it actually doing while it hangs though? Presumably it must be unfolding some definitions, but why?
If b above works, then it doesn't seem to be an instance search issue...?

[Johan Commelin]

I hit this issue very often in LTE. I used the same workaround as Eric: keep the defns a lemma until all the pieces are in place.

[Alex J. Best]

Running the profiler it looks like it is the decl post-processing that hangs?