Zulip Chat Archive

Stream: general

Topic: timeout universe issue


view this post on Zulip Kevin Buzzard (Apr 27 2019 at 15:54):

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.

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 20:05):

@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.

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:06):

I don't really know what this is

view this post on Zulip Kevin Buzzard (Apr 27 2019 at 20:07):

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.

view this post on Zulip Chris Hughes (Apr 27 2019 at 20:09):

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

view this post on Zulip Mario Carneiro (Apr 27 2019 at 20:10):

also how many universe variables are actually in the statement?


Last updated: May 13 2021 at 18:26 UTC