command to generate universe polymorphic inductive failing

Stream: lean4

[Michael Jam]

I'm learning lean 4 meta-programming and as an exercise, I want to generate a structure programmatically from a command.
I'm inside CommandElabM here, so I don't know how to add a definition from syntax. As a result I'm trying to use Environment.addAndCompile stuff to create an inductive definition directly from an internal representation.
I've managed to generate my structure without universes, but I run into problems when I try to add universes in.
Here is my failing mwe:

import Lean
open Lean Elab Command

elab "gen_structure" id:ident : command => do
  let type_u := mkSort (mkLevelSucc (mkLevelParam "u"))
  let decl := mkInductiveDeclEs ["u"] 1 [{
    name := id.getId
    type := mkForall .anonymous .default type_u type_u
    ctors := [{
      name := id.getId ++ "mk"
      type :=
        mkForall "α" .implicit type_u
        <| mkForall "x" .default (mkBVar 0)
        <| mkApp (mkConst id.getId) (mkBVar 1)
    }]
  }] false
  match (← getEnv).addAndCompile {} decl with
  | .error e => throwError ("addAndCompile error: " ++ e.toMessageData {})
  | .ok env => setEnv env

gen_structure struct
#print struct

The error I get is this:

(kernel) incorrect number of universe levels parameters for 'struct', #1 expected, #0 provided

The code works if I replace the universe list ["u"] with an empty list, and (mkLevelParam "u") with levelZero.
It looks like it expects a u variable somewhere but I can't see where. Is it a bug or am I missing something?
Thanks for suggestions. I'm using nightly-2022-05-21

[Mario Carneiro]

If you want to create a definition from syntax in CommandElabM you can do elabCommand <|<- `(def foo : Nat := 1)

[Mario Carneiro]

By the way the usual way to quote names is `x not "x"

[Mario Carneiro]

the issue is that in your mkConst you did not pass the universe parameter. Here's the fixed version:

elab "gen_structure" id:ident : command => do
  let type_u := mkSort (mkLevelSucc (mkLevelParam `u))
  let decl := mkInductiveDeclEs [`u] 1 [{
    name := id.getId
    type := mkForall .anonymous .default type_u type_u
    ctors := [{
      name := id.getId ++ `mk
      type :=
        mkForall `α .implicit type_u
        <| mkForall `x .default (mkBVar 0)
        <| mkApp (mkConst id.getId [mkLevelParam `u]) (mkBVar 1)
    }]
  }] false
  match (← getEnv).addAndCompile {} decl with
  | .error e => throwError ("addAndCompile error: " ++ e.toMessageData {})
  | .ok env => setEnv env

[Mario Carneiro]

@Michael Jam

[Michael Jam]

Thanks Mario, that helps. It seems way more convenient to create a syntax for the code I want and elab it with elabCommand. Using mkInductiveDeclEx and addAndCompile feels too bare bones. One issue I have is that I can't use match on my created structure, it's probably not generating some background stuff that's usually auto generated.
This works:

inductive struct : Type u → Type u | mk {α} : α → struct α
def proj (s : struct α) : α :=
  match s with
  | struct.mk x => x

But this doesn't :

gen_structure struct
def proj (s : struct α) : α :=
  match s with
  | struct.mk x => x

with the following error:

tactic 'cases' failed, not applicable to the given hypothesis, ...

Another problem, is that I am actually implementing an attribute that parses an inductive type to generate a new structure from it, so I'm not in CommandElabM, but in AttrM which doesn't seem to support elabCommand. Is there a way to generate the structure from syntax in AttrM (or CoreM ?)

[Wojciech Nawrocki]

Another problem, is that I am actually implementing an attribute that parses an inductive type to generate a new structure from it, so I'm not in CommandElabM, but in AttrM which doesn't seem to support elabCommand. Is there a way to generate the structure from syntax in AttrM (or CoreM ?)

I know that you can at least run MetaM and TermElabM there, as in this usage example. CommandElabM is probably also possible, but I couldn't immediately find a run/run' method for it.

[Michael Jam]

I could not find a way to elab a command in AttrM/CoreM/MetaM. It seems all the lift / run functions take me away from CommandElabM. I'll try to understand better what all these monads do

[Sébastien Michelland]

This thread should help: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20monads

Additionally, from my (limited) understanding:

• CoreM seems to only provide low-level tools like the environment and timeout systems
• MetaM gives you normalization, definitional equality, type inference and typeclass resolution. See also this. All the meta-level code I've encountered so far runs in it.
• TermElabM is (unsurprisingly) used for term elaboration, it gives you access to term utilities like metavariables, coercions, etc. You usually get there by elaborating syntax rules for terms (eg. macro_rules or the term elab attribute).
• CommandElabM is for command elaboration. It doesn't depend on TermElabM but it still has a method to run term elaboration so you still have access to term utils. You usually get there with the elab or elab_rules command, or the command elab attribute.

Syntax quotations `() are available at several levels, see here.