Zulip Chat Archive

Stream: lean4

Topic: What is `_uniq`?

Eric Rodriguez (Oct 18 2023 at 18:53):

I can share a repro of this (very much not minimised), but I have a bug that (as far as I can tell) depends only on _uniq terms. I'm really not sure what these are and I cannot find much documentation on them, but they're causing really bizarre behaviour in my case. So what are they? Why does rw introduce them?

Henrik Böving (Oct 18 2023 at 18:58):

_uniq are names automatically introduced by the elaborator for free variables, they can definitley pop up in meta code but you'll have to be more precise for help I think.

Eric Rodriguez (Oct 18 2023 at 18:58):

They're popping up in terms in my proof. I will post the whole code in a sec, then

Eric Rodriguez (Oct 18 2023 at 21:44):

Eric Rodriguez (Oct 18 2023 at 21:45):

A very not minimised example; the term is long on purpose to make sure that it's identical in pretty much all other ways.

Eric Rodriguez (Oct 18 2023 at 21:45):

https://www.diffchecker.com/JvUutdxZ/

Eric Rodriguez (Oct 18 2023 at 21:45):

The diff between key and key3 on pp.all for those who can't be asked

Eric Rodriguez (Oct 18 2023 at 21:46):

It is _only_ these uniq terms

Eric Rodriguez (Oct 18 2023 at 21:46):

But if yousee, the rw at the bottom fails on key but succeeds on key3

Eric Rodriguez (Oct 18 2023 at 21:46):

I'm trying to find smaller examples but have failed so far.

Thomas Murrills (Oct 19 2023 at 03:59):

Digging into the code a bit, we can see that rw ... at uses replaceLocalDecl, which in turn contains the following telling comment in replaceLocalDeclCore:

    -- `typeNew` may contain variables that occur after `fvarId`.
    -- Thus, we use the auxiliary function `findMaxFVar` to ensure `typeNew` is well-formed at the position we are inserting it.

Indeed, moving the let inst statement to before have key ... fixes the issue, and now what used to be an unknown free variable is inst. That suggests to me that this part of replaceLocalDeclCore isn't working as intended. Why, exactly, though, I'm not sure yet.

Thomas Murrills (Oct 19 2023 at 06:08):

Oh, looks like a missing instantiateMVars. Some tracing showed me that one of the expressions containing the unknown fvar is actually an mvar (and so the search by findMaxFVar can't see through it). I think what's happening is that the instantiateMVars occurs too early in MVarId.rewrite; we do a bunch of things which can assign mvars after it and thus introduce an fvar.

Maybe replaceLocalDecl should perform an instantiateMVars before it looks for the max fvar in general to bulletproof it against this sort of thing.

Thomas Murrills (Oct 19 2023 at 06:24):

#mwe:

class Bar (α) where a : α

def f {α} [Bar α] (a : α) := a

def w (_ : Nat) : Prop := True

theorem foo {α} [Bar α] (a : α) : a = f a := sorry

set_option pp.explicit true in
example := by
  have h : w 5 := trivial
  let inst : Bar Nat := ⟨0⟩
  rw [foo 5] at h
  /-
  h✝: w 5
  h: w (@f Nat _uniq.124 5)
  inst: Bar Nat := @Bar.mk Nat 0
  ⊢ ?m.95
  -/

Thomas Murrills (Oct 19 2023 at 06:44):

So, to sum up what's happening here and answer the original question more fully:

_uniq appeared because rw tried to use a free variable earlier than it actually appeared in the tactic state.

Under the hood, each free variable consists of a unique id called the FVarId, normally of the form _uniq.NNNN. The local context is what associates those unique id's to surface-level names, like h and inst, as well as to their types.

When you write rw ... at h, rw tries to to replace the free variable with name h with one that has a rewritten type. The types of free variables can't depend on free variables which come after them—only on ones which come before. So, when it replaces h with the new free variable, it tries to take care to insert the new, type-rewritten free variable h after any free variables on which it depends (in this case inst), and then removes the original h.

But because of a bug, it failed at this task: it didn't think that inst was involved in h's type, and thus inserted the rewritten h before inst. (h depends on inst, and so needs to come after inst.) This insertion actually also served to change the FVarId of inst to something else (this is typical; FVarIds might get changed by tactics even if nothing seems like it's visibly changing), so what you're seeing as _uniq.124 is actually the old FVarId of inst before the rewrite—which no longer exists in the local context, and thus gets printed as its raw, underlying FVarId, instead of a nice user-friendly name.

Thomas Murrills (Oct 19 2023 at 07:18):

Issue: lean4#2711

Thomas Murrills (Oct 19 2023 at 08:26):

PR: lean4#2712

Eric Rodriguez (Oct 19 2023 at 08:41):

Wow, Thomas, I was not expecting a full minimsation AND fix whilst I was asleep. Thank you so much! This is amazing, amazing work

Thomas Murrills (Oct 19 2023 at 09:55):

Thanks, but don’t get too excited yet! :D Turns out that while this was indeed a problem, it actually might not be the only problem!

Thomas Murrills (Oct 19 2023 at 12:22):

Where I’m at currently: the minimized version above actually behaves a little differently. The metavariables in foo 5 get created when foo 5 gets elaborated as opposed to from a forallMetaTelescope during the rewrite. Somehow, the metavariable for Bar Nat makes it all the way through to the expression type without being assigned, added to the tactic state, or causing an error.

But there is one thing I really don’t understand: it shows up in the infoview as one of the free variables in its context even though it doesn’t get assigned! All I can guess at is that this has something to do with local instances, since I don’t know what those are really for either (and the fvar does show up in the local instances).

Thomas Murrills (Oct 19 2023 at 21:18):

Ah: the reason it gets replaced with one of its free variables is Term.withSynthesize. Maybe that's part of the issue here...

Thomas Murrills (Oct 20 2023 at 18:51):

Getting closer to figuring out this bug! The issue seems to be that when a local declaration’s type involves a pending metavariable which can be solved by one of its own local instances (via Term.synthesizeSyntheticMVars), but this instance fvar comes after the fvar in question in the original tactic state, we get an unknown free variable in its place. (I.e., just that local instance, but now we don’t know what it is.)

Whether this is a fully accurate characterization of the issue and why this happens exactly, I’m still not sure.

Thomas Murrills (Oct 20 2023 at 19:07):

There’s an easy fix for rw in particular: just perform replaceLocalDecl outside of Term.withSynthesize. But maybe this situation warrants closer attention in general, as it turns hypothesis manipulation within Term.withSynthesize into a bit of a footgun. I’ll open an issue, but I’m not sure what would need to change exactly.

Thomas Murrills (Oct 21 2023 at 07:01):

Issue lean4#2727

Kevin Buzzard (Oct 21 2023 at 07:26):

Is that lean4#2727? And amazing for getting to the bottom of this! Very nice!

Thomas Murrills (Oct 21 2023 at 08:13):

It is indeed! Not the first time I've forgotten the prefix :sweat_smile:

Thomas Murrills (Oct 21 2023 at 08:13):

And here's PR lean4#2728 for this issue in rw specifically, even though it doesn't address the general case of hypothesis manipulation inside Term.withSynthesize. Here's hoping it passes CI. :)

Kevin Buzzard (Oct 21 2023 at 08:14):

It wasn't the last either ;-)

Thomas Murrills (Oct 21 2023 at 08:26):

The Nix build passed, so in a bench or two lean4#2712 and lean4#2728 should be out for review. :)

Eric Rodriguez (Oct 21 2023 at 09:04):

Thank you very much again for investigating and fixing this so promptly, the issues that this bug caused were absolutely horrid to work around! I'm surprised this wasn't run into elsewhere

Thomas Murrills (Oct 21 2023 at 09:30):

No problem! :) Though…we’re not at the finish line yet! It’s only done when it’s merged. :) Looks like the more innocuous change—instantiating mvars—somehow breaks std4. It’s possible this is actually due to some other commit somewhere, but it does look mvar related. :(

I wouldn’t have thought instantiating mvars would be an issue, but maybe it messes with the types or something? I’ll continue investigating tomorrow.

Thomas Murrills (Oct 21 2023 at 09:34):

Actually I’m kind of hopeful that this doesn’t have to do with my change. The declaration

theorem mod_def (a m : Fin n) : a % m = Fin.mk ((a % m) % n) (Nat.mod_lt _ a.size_pos) := rfl

breaks, and I’m not sure how that involves replaceLocalDecl at all…but I haven’t deconstructed it.

Thomas Murrills (Oct 21 2023 at 09:40):

(And it does look like there have been some recent mod-related core commits, so, maybe this is really just an unrelated breakage?)

Mario Carneiro (Oct 21 2023 at 09:48):

That is unrelated breakage; I think there is a PR with the std4 fix to be merged on the next lean bump

Thomas Murrills (Oct 21 2023 at 20:31):

Hmm, I'm trying to get it building by hand, but it's getting a bit difficult to keep up with all of the different adaptations that need to be manually incorporated. For example, I merged that std4 PR into a branch on my fork, then updated the testing branch to use that fork; but then mathlib4 was broken in two different ways still unrelated to the lean4 PR at hand (upstreaming of lemmas, and something involving sublists).

Scott Morrison (Oct 21 2023 at 23:58):

Sorry, it's the weekend here, and a breaking change was committed late Friday... :-( Hopefully nightly-testing is now working, but there are probably a bunch of lean-pr-testing-NNNN branches that need to have nightly-testing merged into them.

Thomas Murrills (Oct 22 2023 at 00:36):

Ah, sorry! In general, is waiting a while then merging nightly-testing into the pr testing branch the way to go? Do the lean4 PRs also need to be rebased onto master when doing that? (Does the latter trigger the former automatically?) (At your leisure—I’m not in any rush :) )

Scott Morrison (Oct 22 2023 at 00:50):

Unfortunately, the only way to be completely certain that lean-pr-testing-NNNN branches are behaving properly is:

  • Check that nightly-testing is currently building.
  • Check that your lean4 PR is rebased onto the commit corresponding to the nightly release that nightly-testing is using.
  • Merge nightly-testing into your lean-pr-testing-NNNN branch.

As an approximation to that:

  • rebasing your lean4 PR onto master, and/or
  • merging nightly-testing into your lean-pr-testing-NNNN branch
    are nearly always helpful if you have a mysterious failure on your lean-pr-testing-NNNN branch. :-)

Last updated: Dec 20 2023 at 11:08 UTC