Local definition generalization and possible TDNR improvement

[dolio]

This PR is the result of my work investigating and fixing #3752. The fix to that was to generalize non-recursive let in the type checking code path. However, in getting that to actually work, I had to tweak some other aspects of the type checker as well.

I factored out the code for generalizing let in the synthesis path. However, I believe it wasn't correct. For instance, I think it would generalize a let like:

r = Scope.ref '(bug "whatever")

When you do this, you get r : forall a. Ref {Scope} 'a, which can then be used to coerce between any two types. To avoid this, I do not generalize when the right hand side requires abilities. Note though that this allows lambda terms to be generalized, so it's probably not a very significant limitation.

I think the old generalization code would also produce bad TDNR results. There was a check to see if the RHS was, 'closed,' which meant it contains free variables that weren't previously type checked. However, TDNR candidates are not actually represented as variables, they are 'blank' terms. So the old code would generalize, and probably prevent any information from flowing into the actual TDNR solution.

Instead, my new strategy is to only generalize over some variables (and the 'closed' check has just been removed). The context actually keeps track of which variables come from a TDNR candidate. So, when we move out of the scope of the binding's body, I look at the discarded context, and find all variables that are used in the TDNR candidate's type. These are not generalized over, while other variables are. This allows the body of the let to contribute to solving the TDNR candidate's type.

The handling of the saved TDNR data has also been improved. Whenever we discard a portion of context with a TDNR type in it, we take a snapshot of the type at that point. However, this is just as problematic as the generalization above would be. The snapshot is never refined by later instantiations. So, I have updated it so that when we do context discards, we substitute into the TDNR info, which lets us retain any information we've figured out about the types.

Fixes #3752
Improves the error message in #4456

[pchiusano]

Nice! Glad this worked out.

[aryairani]

Heads up that CI failed in the jit tests, not sure if it's a false positive or what: https://github.com/unisonweb/unison/actions/runs/7658151250/job/20870460454?pr=4642

[dolio]

Yeah, I saw. I think something in there is more monomorphic than it previously was. So either I need to add a signature or tweak my new strategy a little more.

[dolio]

I realized, the error message is accurate in 4456 with this PR. So:

Fixes #4456
Fixes #4638 (a duplicate)

[dolio]

Okay, hopefully this is complete now (once I fix some warnings).

I realized that I was missing some parts of the context that would be relevant to refining the TDNR solutions. So it was possible to confuse the checker by nesting lets and stuff within one another. For example, a case like:

foo i =
  bar j =
    k = i + j
    k
  bar 1

Would not be able to figure out +. So, I added a new sort of Blank to indicate that we should keep a variable around for informing TDNR, and re-mark some upper portions of the context with these if they're generic blanks. Let me know if something doesn't look right with that.

[pchiusano]

Nice. I'd say merge once CI passes.