timeout universe issue

Stream: general

[Kevin Buzzard]

I have spent many hours over the last few weeks trying to make this compile (from deep within the perfectoid project):

noncomputable def valuation_on_completion {R : Type*} [comm_ring R] (v : valuation R Γ) :
  valuation
    (ring_completion
      (valuation.valuation_field v))
    (value_group v) :=
valuation.completion_extend (valuation_field.canonical_valuation v)

I would get deterministic timeouts which were extremely hard to debug.

Today I idly changed Type* to Type u and all the issues immediately went away.

Thanks Lean.

[Kevin Buzzard]

@Simon Hudon @Mario Carneiro is this a known bug in Lean 3.4.2? Can this be fixed in Lean 3.5c? I know Kenny found some universe weirdness but I didn't remember it being as harsh as this.

[Mario Carneiro]

I don't really know what this is

[Kevin Buzzard]

Kenny also had an example where elaboration behaved differently when universes were mentioned explicitly. We've been struggling with a "heavy rfl" for days now, and today it just magically went away when I randomly tried this. We were on the verge of proclaiming that perfectoid spaces created terms which type class inference simply could not handle, but then all our problems seemed to magically go away when I switched. This issue has been kind of a big deal in my life over the last two weeks and I'm extremely glad to see the back of it.

[Chris Hughes]

Did the Type* fill it in correctly. I had this problem where it guessed max u v instead of w.

[Mario Carneiro]

also how many universe variables are actually in the statement?