Tactics and universes

Stream: metaprogramming / tactics

[Pedro Minicz]

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

[Pedro Minicz]

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

[Pedro Minicz]

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

[Pedro Minicz]

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

[Kenny Lau]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

conveniently, these have the same universe level

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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?

[Reid Barton]

I think it is

[Jannis Limperg]

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.

[Mario Carneiro]

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

[Jannis Limperg]

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