feat: Invariance limitations improvements

[Kamirus]

1. When choosing between type T and Any, pick T when it has no proper supertypes (except Any).
   Previously we needed the T to be isolated (no proper subtypes nor supertypes).
   This change allows Int and ?T as well! (Assuming T has no supertypes).
   See the tests for more examples.

Likewise, when choosing between Non and T, pick T when it has no proper subtypes (except Non).

2. Error message improvements:

• We should start to suggest writing a return type annotation and preferring that over a type instantiation. See the lambdas-core.mo test cases e.g. here
• Perhaps we can start suggesting a concrete return type annotation so that it's easier for developers and AI -- they would just need to copy and paste it, perhaps modifying it slightly. This is better than making the compiler make the arbitrary choice. It would just suggest a solution. I think this might be a middle ground between developer experience and forcing the compiler to make an arbitrary choice (when there is no principal solution)
• I think the error message because implicit instantiation of type parameter R is under-constrained with is a bit cryptic, maybe we can find a better alternative that explains that there is no best solution and the compiler won't make an arbitrary choice...

For example (error message improvement)

let _ = VarArray.map(va, func x = x); // Nat

Before

cannot implicitly instantiate function of type
  <T, U>([var T], T -> U) -> [var U]
to argument of type
  ([var Nat], Nat -> U)
because implicit instantiation of type parameter U is under-constrained with
  Nat  <:  U  <:  Any
where
  Nat  =/=  Any
so that explicit type instantiation is required

After

... cannot solve invariant type parameter U, no principal solution with
  Nat  <:  U  <:  Any
where
  Nat  =/=  Any
Add a return type annotation or an explicit type instantiation
Suggested return type annotation : 
  [var Nat]

In the future we could integrate it into the vscode extension to provide a 'quick fix' that would insert this type annotation.
Limitations: The return type might be too long, we would not use type aliases, maybe we should avoid the suggestion when the type is longer than X characters.

[github-actions]

Comparing from 64889ef to 7105c15:
In terms of gas, no changes are observed in 5 tests.
In terms of size, no changes are observed in 5 tests.

[crusso]

Can you do the symmetric thing for Non, t when has_no_subtypes t

[Kamirus]

We could, yes. I just did not see enough examples in practice that would benefit from that. So I wanted to limit this heuristic for now

[Kamirus]

But I guess it makes sense to make it symmetric. the has_no_subtypes is already ignoring the bottom type Non so it should be consistent.
I'll add some examples covering that. I guess something returning a function that takes a mutable data structure 😄

[crusso]

Why only report the first error? To avoid information overload?

[Kamirus]

To retain the original behavior. We could gather all of them and report all. I just needed to finish the building of env so that I have the substitution.

[Kamirus]

OK, I've refactored and now we gather all 'under-constrained' and merge into a single error message, see the test output here

[Kamirus]

@crusso @christoph-dfinity Hm, perhaps now with dot-notation we might actually prefer 'type instantiations' over 'return type annotations' because it is easier to write them with a dot-chain of functions like

list
  .map<X,Y>(func x = ...)
  .filter(func y = ...)
  ...

Though we could probably easily allow partial type instantiations like

list
  .map<_,Y>(func x = ...)

Because only the 2nd type parameter of map on a mutable list is essential to provide