## Stream: metaprogramming / tactics

### Topic: Tactics and universes

#### 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


#### 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?

#### 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


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

#### Kenny Lau (Sep 10 2020 at 16:33):

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

#### 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

#### 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

#### Reid Barton (Sep 10 2020 at 16:35):

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

#### 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

#### 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

#### Simon Hudon (Sep 10 2020 at 17:12):

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

#### Reid Barton (Sep 10 2020 at 17:13):

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

#### Reid Barton (Sep 10 2020 at 17:13):

conveniently, these have the same universe level

#### Simon Hudon (Sep 10 2020 at 17:14):

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

#### Reid Barton (Sep 10 2020 at 17:18):

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

#### Reid Barton (Sep 10 2020 at 17:18):

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

#### 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

#### Simon Hudon (Sep 10 2020 at 17:24):

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

In the VM, both α and uchange α have the same representation.

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

I think it is

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

#### Mario Carneiro (Sep 11 2020 at 15:34):

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

#### 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