this is often due occurs-check failure

Stream: lean4

[Snir Broshi]

What is the error this is often due occurs-check failure supposed to mean? To me it seems like there are grammar issues with this message, but I might be missing something.
I'm not asking how to fix the error in my code, I'm asking whether the message is wrong and we should change it.
Perhaps the message meant to say "this is often caused by other errors, check for more messages above"?

This message is from closeMainGoal and closeMainGoalUsing.

[Snir Broshi]

variable (n : Nat)

/--
error: don't know how to synthesize placeholder
context:
n : Nat
⊢ Nat

Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be
---
error: Tactic `exact` failed: attempting to close the goal using
  sorry
this is often due occurs-check failure

⊢ ?m.2 = 0
-/
#guard_msgs in
theorem foo : _ = 0 := by
  sorry

(btw idk why variable is necessary to reporoduce)

[Aaron Liu]

an occurs-check is a check that the goal is not being used to close itself

[Snir Broshi]

So is the message supposed to be this is often due to an occurs-check failure?

[Snir Broshi]

Also is that term supposed to be user-facing?

[Kyle Miller]

Yes, occurs-check is currently meant to be user-facing, and the original error should read "due to".

The error could say "this is often due to metavariable assignments failing due to the occurs check", with some pointer to documentation that explains that when assigning ?m := e, the expression e cannot have any occurrences of ?m (that's the so-called "occurs check", a key concept in unification). Ideally the error would point out why the occurs check fails.