I believe there are two problems here.

Problem 1: no syntax for non-recursive let

Consider the following term (where bar is a variable).

foo = bar
foo

When parsed, it's represented as (roughly)

Let (Var "bar") (Abs "foo" (Var "foo"))

It looks a little inside-out, but it means:

• Let the next binder be bound to variable "bar"
• foo -> foo

All good so far. Now consider

foo = .foo
foo

Here the RHS of the binder refers to a "foo" defined elsewhere. It's similarly parsed as

Let (Var "foo") (Abs "foo" (Var "foo"))

or

• Let the next binder be bound to variable "foo"
• foo -> foo

Still all good so far. The problem, though, is that when we print this term with its non-recursive let, the syntax doesn't explicitly forbid self-reference. So we end up omitting

foo = foo
foo

which is parsed back as a busted self-reference that's not guarded by a lambda.

Problem 2: variable "resetting"

Consider now a similar situation, but involving a legitimate recursive let. It's a little contrived, but:

foo = do
  _ = foo -- to make foo recursive
  bar
foo()

This is parsed as

Cycle (
  Abs "foo" (
    LetRec 
      [ Lam (Abs Unit (Let (Var "foo") (Abs "_" (Var "bar")))) ]
      (App (Var "foo") Unit)
  )
)

Broken down, that's:

• Introduce the variable "foo" to be in scope for an entire (one-element) cycle
• Define the body of that binding as () -> let _ = foo in bar
• Apply foo to ()

Now if we instead substitute .foo for bar, we'll get something similar:

Cycle (
  Abs "foo¹" (
    LetRec 
      [ Lam (Abs Unit (Let (Var "foo¹") (Abs "_" (Var "foo")))) ]
      (App (Var "foo¹") Unit)
  )
)

Or, back in familiar Unison syntax,

foo¹ = do
  _ = foo¹
  foo
foo¹()

where the binder "foo" has been freshened to "foo¹" so that it doesn't capture the internal free variable "foo".

Ok! but then the issue is that, when printing a term, we explicitly reset all variables with the following justification:

OK since all term vars are user specified, any freshening was just added during typechecking

This comment appears to be incorrect, as in this example we rely on freshening to disambiguate.