feat: Infer invariant when bound is isolated (no proper super/subtypes except Top/Bottom)

[Kamirus]

Allow inference of invariant type variables when the solution has no proper subtypes nor supertypes (except Top/Bottom).
After:

let _ = VarArray.map(va, func x = debug_show(x)); // needs no explicit instantiation

Before:
Since the result of the map function is a mutable array, the type variable in the result is invariant. This causes the following error:

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
  Text  <:  U  <:  Any
where
  Text  =/=  Any
so that explicit type instantiation is requiredMotoko(M0098)

The compiler complains that it cannot solve U as, for example, both Text and Any would fit but they are not equivalent, and U is invariant so the choice matters.

IMO, considering Any as the solution for U is impractical and users would be better off not providing type instantiations in such cases.

However, there is danger in allowing arbitrary types as solutions for invariant type variables, so I propose we restrict these types to "isolated" types (types that have no proper subtypes nor supertypes except Top/Bottom). See the tests for more examples.

[crusso]

At first glance this looks very nice! How do you feel about it?

[crusso]

Curious if the example from #5036 now works.

[Kamirus]

At first glance this looks very nice! How do you feel about it?

I feel good about it, I think this is a good change 😄

[Kamirus]

Curious if the example from #5036 now works.

I've just added a test for it, and yes it does infer now, because the bound was Text

[crusso]

@christoph-dfinity whaddya think? I like it...but maybe you can see a downside.

[christoph-dfinity]

Code changes look good. I think I can follow the reasoning and motivation as well, so LGTM!