Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Tactics and universes


view this post on Zulip Pedro Minicz (Sep 10 2020 at 16:30):

Why does the following not work?

import tactic

open expr tactic

meta def {u} focus {α : Type u} (tac : tactic α) : tactic α :=
do g :: gs  get_goals,
   set_goals [g],
   a  tac,
   new_gs  get_goals,
   set_goals (new_gs ++ gs),
   return a

view this post on Zulip Pedro Minicz (Sep 10 2020 at 16:31):

Looking at the definition of focus1, it seems to only work for Type (aka Sort 1). Isn't that somewhat limiting?

view this post on Zulip Pedro Minicz (Sep 10 2020 at 16:32):

What makes this intriguing is that the following works:

meta def focus {α : Type*} (tac : tactic α) : tactic α :=
do g :: gs  get_goals,
   set_goals [g],
   a  tac,
   new_gs  get_goals,
   set_goals (new_gs ++ gs),
   return a

view this post on Zulip Pedro Minicz (Sep 10 2020 at 16:32):

Declaring u in a standalone universe u declaration before the definition doesn't fix the problem in the first example.

view this post on Zulip Kenny Lau (Sep 10 2020 at 16:33):

can you be more specific than "doesn't work"?

view this post on Zulip Reid Barton (Sep 10 2020 at 16:33):

Pedro Minicz said:

What makes this intriguing is that the following works:

Right, because Type* means Lean gets to pick the universe level and it picked the only possible one, namely Type

view this post on Zulip Reid Barton (Sep 10 2020 at 16:34):

Pedro Minicz said:

Looking at the definition of focus1, it seems to only work for Type (aka Sort 1). Isn't that somewhat limiting?

Yes, somewhat, but it's hard to get monads to play along with universes IIRC

view this post on Zulip Reid Barton (Sep 10 2020 at 16:35):

and normally Type would be adequate for anything you actually want to pass around at runtime

view this post on Zulip Simon Hudon (Sep 10 2020 at 16:59):

Reid Barton said:

Yes, somewhat, but it's hard to get monads to play along with universes IIRC

Addendum: that is indeed true but it can be done if it's necessary. If not, use Type and your design will be simpler for it. If you really need universe polymorphism in tactic for whatever reason, use tactic.up and tactic.down: https://github.com/leanprover-community/lean/blob/1604446600dd4249fc5d5570373e4d62e4eb469d/library/init/meta/tactic.lean#L75

In other monads, there's uliftable which is quite cumbersome: https://github.com/leanprover-community/mathlib/blob/master/src/control/uliftable.lean

view this post on Zulip Reid Barton (Sep 10 2020 at 17:01):

As I recall it's also possible to defeat the universe level checks in meta and stuff your large data in a Type

view this post on Zulip Simon Hudon (Sep 10 2020 at 17:12):

@Reid Barton can you elaborate? Would you for instance unsafe_coerce to unit and then back?

view this post on Zulip Reid Barton (Sep 10 2020 at 17:13):

I think you can coerce id : Type u -> Type u to have type Type u -> Type

view this post on Zulip Reid Barton (Sep 10 2020 at 17:13):

conveniently, these have the same universe level

view this post on Zulip Simon Hudon (Sep 10 2020 at 17:14):

I don't think that's a limitation for unsafe_coerce though

view this post on Zulip Reid Barton (Sep 10 2020 at 17:18):

Oh, it's even in mathlib: docs#uchange

view this post on Zulip Reid Barton (Sep 10 2020 at 17:18):

Change universe levels using this one weird trick mathematicians don't want you to know about

view this post on Zulip Reid Barton (Sep 10 2020 at 17:20):

Simon Hudon said:

I don't think that's a limitation for unsafe_coerce though

Maybe not in Lean 4? The Lean 3 implementation uses cast with an unsound proof of equality in Type u, so it needs the universes to agree

view this post on Zulip Simon Hudon (Sep 10 2020 at 17:24):

My mistake, I thought they didn't need to agree.

[from the link]
In the VM, both α and uchange α have the same representation.

I always assumed that was also the case for ulift. Is it not?

view this post on Zulip Reid Barton (Sep 10 2020 at 17:26):

I think it is

view this post on Zulip Jannis Limperg (Sep 11 2020 at 15:34):

Shouldn't universe levels just be ignored in meta land instead of this uchange thing? Pretend that every sort is Type whenever we're in a meta def and disable universe checking in meta inductive. Maybe the distinction between Prop and Type needs to be kept, but the Type tower should collapse.

view this post on Zulip Mario Carneiro (Sep 11 2020 at 15:34):

I think this is easier said than done because it kind of breaks the typechecker

view this post on Zulip Jannis Limperg (Sep 11 2020 at 15:35):

Possible. I haven't thought through this in any detail.


Last updated: May 09 2021 at 22:13 UTC