Transitive isAssigned

Stream: lean4

[Marcus Rossel]

When assigning an mvar m₂ whose type also contains an mvar m₁, how can I check whether m₁ has been assigned (by virtue of m₂ being assigned)? I tried the following, but that leads to m₁ being considered unassigned:

import Lean
open Lean Meta Elab Term

elab "test" : term => do
  let m₁ ← mkFreshExprMVar (Expr.sort 1)
  println! ← m₁.mvarId!.getType
  -- Type

  let m₂ ← mkFreshExprMVar (Expr.app (.const ``List [← mkFreshLevelMVar]) m₁)
  println! ← m₂.mvarId!.getType
  -- List.{?_uniq.2855} ?_uniq.2854

  let l ← elabTerm (← `(([] : List Nat))) none
  let l ← instantiateMVars l
  println! ← inferType l
  -- List.{0} Nat

  m₂.mvarId!.assign l
  let m₂ ← instantiateMVars m₂
  println! ← inferType m₂
  -- List.{0} Nat

  println! ← m₁.mvarId!.isAssigned
  -- false

  return mkNatLit 0

example := test

[Marcus Rossel]

Ahhh, the docs for docs#Lean.MVarId.assign hold the answer: "This is a low-level API, and it is safer to use isDefEq (mkMVar mvarId) x" :see_no_evil:.

[Mario Carneiro]

That documentation is lying, don't do that

[Mario Carneiro]

I think there is an open issue about it

[Mario Carneiro]

The problem is that isDefEq (mkMVar mvarId) x doesn't assign the mvar at all if it's a proof

[Mario Carneiro]

instead you should use assignIfDefeq

[Mario Carneiro]

Although, reading your question I don't see what it has to do with assign

[Mario Carneiro]

mvar.isAssigned should return true if and only if mvar is assigned. I don't really understand what you mean by "m₁ has been assigned (by virtue of m₂ being assigned)"

[Mario Carneiro]

I can't find assignIfDefeq though, maybe it's too new (or the PR stalled)? In any case, in your code you need to make sure the types match before the assign call, i.e.

  let .true ← isDefEq (← inferType m₂) (← inferType l) | failure
  m₂.mvarId!.assign l

[Marcus Rossel]

Mario Carneiro said:

mvar.isAssigned should return true if and only if mvar is assigned. I don't really understand what you mean by "m₁ has been assigned (by virtue of m₂ being assigned)"

Then it seems I don't understand what it means for an mvar m to be "assigned". I thought it means that there's a value associated with m in the current mvar context. That is, if I used instantiateMVars on an expression containing m, then m would be replaced by something else. How do I check for this notion of being assigned (and what is it called)?

[Marcus Rossel]

Mario Carneiro said:

I can't find assignIfDefeq though, maybe it's too new (or the PR stalled)?

It's in Std.Tactic.Exact.

[Mario Carneiro]

that is correct

[Mario Carneiro]

the issue is that, as the doc says (before making a misleading suggestion), assign is a low level function, and in particular it has a precondition that the types match

[Marcus Rossel]

Mario Carneiro said:

that is correct

Ah, then I guess my wording was just bad. What I mean is that isAssigned can propagate, and can become true for mvars as a result of other mvars being assigned. Would you say that's correct?

[Mario Carneiro]

No, assigning mvars does not cause other mvars to be assigned

[Mario Carneiro]

isDefEq calls can cause mvars to be assigned

[Mario Carneiro]

if you do not already know in advance that the types match, you should call isDefEq before assign (or use assignIfDefeq which does both)

[Marcus Rossel]

If isDefEq assigns mvars, why is assign necessary afterwards? (aside from "The problem is that isDefEq (mkMVar mvarId) x doesn't assign the mvar at all if it's a proof")

[Mario Carneiro]

that's why

[Mario Carneiro]

note that I didn't use isDefEq on the value itself, I used it on the types

[Marcus Rossel]

ok, so in a perfect world we never call assign explicitly?

[Mario Carneiro]

in a surprisingly large number of situations you know the types match for structural reasons

[Mario Carneiro]

I thought that we would be using assignIfDefeq more in core but I audited all the uses and most of them can actually safely be assign

[Marcus Rossel]

But even then, assign doesn't do the isAssigned propagation that I'm looking for. Can I cause this propagation to happen after using assign?
(I'm also in a situation where I know the types match)

[Mario Carneiro]

the types in your example don't match, that's the point

[Mario Carneiro]

or at least, they don't match until some variables are assigned

[Mario Carneiro]

so that's what isDefEq does

[Mario Carneiro]

if you assign an mvar before making the types match then you end up in an invalid state

[Marcus Rossel]

Ok, I thought "types matching" meant "matching up to mvar assignment" :sweat_smile:

[Marcus Rossel]

I think now everything is clear. Thanks for your help!