Strange excessive memory consumption

Stream: general

[Michael Stoll]

import number_theory.cyclotomic.basic

def test {F : Type} [field F] : cyclotomic_field 8 F :=
begin
  let χ := algebra_map ℤ (cyclotomic_field 8 F),
  sorry
end

produces (after more than half a minute)

excessive memory consumption detected at 'replace'

but

import number_theory.cyclotomic.basic

def test {F : Type} [field F] : cyclotomic_field 8 F :=
begin
  let χ := algebra_map ℤ (cyclotomic_field 8 F),
  exact χ 17,
end

works fine.
What is going on here?

[Riccardo Brasca]

This can be related with a diamond about the ℤ-algebra structure. What happens if you open_localy cyclotomic?

[Alex J. Best]

I think its the noncomputabiliy checker again

import number_theory.cyclotomic.basic
.
noncomputable!
def test {F : Type} [field F] : cyclotomic_field 8 F :=
begin
  let χ := algebra_map ℤ (cyclotomic_field 8 F),
  sorry
end

works as intended

[Riccardo Brasca]

Ah you're right

[Michael Stoll]

OK, thanks. I'll try to remember using noncomputable! when I get such errors.