Prevent the creation of new synthetic mvars

Stream: lean4

[Leni Aniva]

Suppose we have an expression like this

fun (p q: Prop) => (1: Nat)

and during the call to Meta.transform on this function, the pre phase converts (1: Nat) to ?m.1 p q, where ?m.1 is some delayed assigned metavariable dependent on some context.

When Meta.transform finishes with the lambda, it converts ?m.1 p q to another delayed assigned metavariable, ultimating resulting in

fun (p q: Prop) => ?m.3 p q p q

I suspect this is because ?m.1 p q refers to p and q, so Lean creates a delayed assigned metavariable for it.

Is there a way to get fun (p q: Prop) => ?m.1 p q instead?

[Leni Aniva]

The context of this problem is I want to merge chains of delayed assigned metavariables. For example if

?m.1 := ?m.2 [_f.10 := ...]
?m.2 := ?m.3 [_f.11 := ...]

then the result of the merger should be

?m.4 := ?m.3[_f.10 := ..., ?f.11 := ...]

[Leni Aniva]

I have a partial solution to this problem: Instead of creating delayed assigned metavariables, use (← Meta.mkLambdaFVars fvars inner).beta args, where inner is an expression that could contain metavariables in principle. This automatically handles the creation of metavariables.

The problem about this approach is sometimes mkLambdaFVars creates additional mvars that are not assigned or delayed assigned. For example

Eq.{?_uniq.83} ?_uniq.87 ?_uniq.88 ?_uniq.89

after mkLambdaFVars, I got

Eq.{?_uniq.83} (?_uniq.90 ?_uniq.68) (?_uniq.91 ?_uniq.68) (?_uniq.92 ?_uniq.68)

where ?_uniq.{90,91,92} are not assigned or delayed assigned. This is very strange to me since it cuts off the connection between this expression and ?_uniq.{87,88,89}.

It is very difficult to get a MWE from this since this behaviour vanishes for smaller examples

[Leni Aniva]

this check returns true, showing that the variables are unrelated

occursCheck { name = "_uniq.87".toName} (.mvar { name = "_uniq.90".toName })

as well as this one

occursCheck { name = "_uniq.87".toName} e

where e is `Eq.{?_uniq.83} (?_uniq.90 ?_uniq.68) (?_uniq.91 ?_uniq.68) (?_uniq.92 ?_uniq.68).

so in this case mkLambdaFVars has decoupled a dependency of its input expression

[Leni Aniva]

This is the function I am using to force the instantiation of delayed mvars:

partial def instantiateDelayedMVars (eOrig: Expr) (level := 0): MetaM Expr := do
  let padding := String.join $ List.replicate level "│ "
  IO.println s!"{padding}Starting {toString eOrig}"
  let mut result ← Meta.transform (← instantiateMVars eOrig)
    (pre := fun e => e.withApp fun f args => do
      let .mvar mvarId := f | return .continue
      IO.println s!"{padding}├V {e}"
      let mvarDecl ← mvarId.getDecl

      let lctx ← MonadLCtx.getLCtx
      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
          | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
          | .none => acc) []
        panic! s!"Local context variable violation: {violations}"

      if let .some assign ← getExprMVarAssignment? mvarId then
        IO.println s!"{padding}├A ?{mvarId.name}"
        assert! !(← mvarId.isDelayedAssigned)
        return .visit (mkAppN assign args)
      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
        let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
        IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"

        if args.size < fvars.size then
          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
        if !args.isEmpty then
          IO.println s!"{padding}├── Arguments Begin"
        let args ← args.mapM self
        if !args.isEmpty then
          IO.println s!"{padding}├── Arguments End"
        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
          IO.println s!"{padding}├T1"
          let result := mkAppN f args
          return .done result

        let pending ← mvarIdPending.withContext do
          let inner ← instantiateDelayedMVars (.mvar mvarIdPending) (level := level + 1)
          IO.println s!"{padding}├Pre: {inner}"
          let r ← Meta.instantiateLambda (← Meta.mkLambdaFVars fvars inner) args
          pure r

        -- Tail arguments
        let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
        IO.println s!"{padding}├MD {result}"
        return .done result
      else
        assert! !(← mvarId.isAssigned)
        assert! !(← mvarId.isDelayedAssigned)
        if !args.isEmpty then
          IO.println s!"{padding}├── Arguments Begin"
        let args ← args.mapM self
        if !args.isEmpty then
          IO.println s!"{padding}├── Arguments End"

        IO.println s!"{padding}├M ?{mvarId.name}"
        return .done (mkAppN f args))
  IO.println s!"{padding}└Result {result}"
  return result
  where
  self e := instantiateDelayedMVars e (level := level + 1)