Fully apply ctor to mvars

Stream: lean4

[Marcus Rossel]

Given a constructor name ctor, is there a good way to construct an Expr which represents a full application of ctor to fresh mvars? For example, given Prod.mk, I would like to construct @Prod.mk.{?u1, ?u2} ?m1 ?m2 ?m3 ?m4. I tried the following for a simpler example:

import Lean
open Lean Meta

structure S where
  a : Nat
  b : Bool

#eval do
  let some (.ctorInfo ctorInfo) := (← getEnv).find? ``S.mk | throwError "failed"
  let fieldMVars := List.toArray <| List.replicate ctorInfo.numFields (← mkFreshExprMVar none)
  let e ← mkAppM ``S.mk fieldMVars
  return e

... but that fails because mkAppM doesn't seem to be happy about the mvars' types.

The only other way I can think of right now is to forallMetaTelescope on the type of ctor to get mvars with proper types. But then I'm still not sure how to construct the application.

[Aaron Liu]

This was unexpectedly difficult

import Lean
open Lean Meta

structure S where
  a : Nat
  b : Bool

#eval do
  let some (.ctorInfo ctorInfo) := (← getEnv).find? ``S.mk | throwError "failed"
  let fieldMVars ← (List.replicate ctorInfo.type.getForallArity ()).mapM (fun _ => mkFreshExprMVar none)
  let e := mkAppN (.const ``S.mk (← mkFreshLevelMVarsFor (.ctorInfo ctorInfo))) fieldMVars.toArray
  check e
  let e ← instantiateMVars e
  return e

[Mario Carneiro]

#eval do
  let info ← getConstInfo ``S.mk
  let ls ← mkFreshLevelMVarsFor info
  let (xs, _) ← forallMetaTelescope (info.type.instantiateLevelParams info.levelParams ls)
  return mkAppN (.const info.name ls) xs

[Marcus Rossel]

There's always more metaprogramming API out there, isn't there :sweat_smile: