Extract and instantiate metavariables of a type

Stream: metaprogramming / tactics

[Chris Henson]

Is there a standard way to extract (and instantiate ) all metavariables in a type? For example, assume that I have some existing type variables (A B ... : Type) that I want to use in ?α, ?α × ?β, ..., List ?α, List (?α × ?β), List (?α × ?β × ?γ), etc. The assumption here is that the only metavariables are these type variables

[Kyle Miller]

Could you say a bit more about the context of what you're doing?

[Chris Henson]

The gist is that I'd like to write a macro to insert some typeclass instances that are basically serving as type hints. Something like:

class Foo (X : Type)
class Hint (X : Type)

-- I'd like a macro where `add_hint List (?α × ?β)` expands to
instance [Hint A] [Hint B] : Foo (List A × B) where

[Daniel Weber]

See https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/CollectMVars.html

[Kyle Miller]

What is the actual output you want? A new instance? Or instance syntax with a "try this"-like functionality?

[Chris Henson]

If there is another way to hint to typeclass inference to

Daniel Weber said:

See https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/CollectMVars.html

This looks helpful, thanks!

[Kyle Miller]

Could you clarify your first sentence @Chris Henson ? Sorry, I'm not following what you mean.

[Kyle Miller]

Anyway, there are some limitations with this (namely mkAppM can fail because it won't assign universe level variables, which is fixable), but a metaprogramming approach can be to use metavariable abstraction functions:

class Foo (X : Type _)
class Hint (X : Type _)

open Lean Elab Command Term Meta
elab "add_hint " t:term : command => do
  runTermElabM fun args => do
    let ty ← elabType t
    synthesizeSyntheticMVarsNoPostponing
    let res ← abstractMVars ty (levels := false)
    lambdaBoundedTelescope res.expr res.numMVars fun margs expr => do
      let newDecls ← margs.mapM fun marg => do
        pure (← mkFreshUserName `inst, BinderInfo.instImplicit,
          fun _ => do mkAppM `Hint #[← inferType marg])
      withLocalDecls newDecls fun hints => do
        let ty ← mkForallFVars (args ++ margs ++ hints) (← mkAppM `Foo #[expr])
        logInfo m!"hinted type is {ty}"


add_hint List (?α × ?β)
/-
hinted type is (α : Type ?u.5137) →
  (β : Type ?u.5136) → [inst : Hint (Type ?u.5137)] → [inst : Hint (Type ?u.5136)] →
  Foo (List (α × β))
-/

variable (n : Nat)
add_hint List ?α → Fin n
/-
hinted type is (n : ℕ) → (α : Type ?u.5155) → [inst : Hint (Type ?u.5155)] → Foo (List α → Fin n)
-/

[Chris Henson]

Kyle Miller said:

Could you clarify your first sentence Chris Henson ? Sorry, I'm not following what you mean.

No worries, I'm new to the metaprogramming and probably a bit unclear. Let me try explaining again.

In my actual use case, I'm trying to tag these certain type variables to be used in some other typeclass inference. I'm doing so via this empty Hint typeclass, which works fine but is a bit clunky. So I'd just like that a macro so that calling add_hint T, extract all metavariables from T (which I think the suggestion from Daniel does) and end up expanding to the output instance instance [Hint A] [Hint B] ... : Foo T, where I have instantiated all the type metavariables in T.

Very likely not the "right" think to do, I'm just learning what's possible at this point.

[Kyle Miller]

To be clear, when you say "expand", you mean update the source code right? There are multiple levels of representation, and it matters a lot which you want to operate on.

[Kyle Miller]

If it's just at the Syntax level, you can avoid touching Meta stuff completely.

[Kyle Miller]

I see you did say "macro", did you mean that in the Lean macro sense?

[Chris Henson]

Kyle Miller said:

I see you did say "macro", did you mean that in the Lean macro sense?

Okay took me a bit to walk through your code, but I think I mostly understand. I think elab would have been more accurate to say. (Thanks for your patience, still learning the verbiage!) I think your code is doing roughly what I was thinking, though I did mean just creating a new instance. A couple of questions. This constructs and works with the instances locally for the logging, but if I wanted, I could just silently create this instance, right? I also don't quite get what you mean about "just at the Syntax level", you mean a different approach that manipulates just the syntax that happens to have metavariables in it?

[Kyle Miller]

Yes, you can manipulate the ?x syntax directly, without actually working with metavariables per se. Take a look at the implementation of the docs#Mathlib.Tactic.congrM syntax for an example. You could construct an instance Syntax and then elaborate that with docs#Lean.Elab.Command.elabCommand

[Chris Henson]

Okay that makes sense and seems nicer in some ways. In contrast If I were to build from your example using metavariables, I would create the instance there too using something like docs#Lean.Meta.addInstance, right?

[Kyle Miller]

addInstance would be the last step, after actually defining the function and adding it to the environment. It tends to be easier to make macros that just ask def/instance/etc. to handle everything for you.