Importing a rigid variable in a non-generalized context should not keep
the variable as rigid. That's because rigid variables are only necessary
for enforcing invariants during typechecking of a generalizable
definition, but at all use sites (which are not generalized), they are
demoted to possibly-unbound type variable.
Many times, in order to create a `ven_pretty::Doc` containing a text
node, the pattern `alloc.text(format!(...))` would be used. This code
then creates a fresh string that is then used in the `Doc`. However,
many times only a small string is necessary and so the allocation could
be optimized. The `ven_pretty` crate supports this through a `SmallString`
type. Allocating a fresh string with `format!` also moves control away
from the `DocAllocator` which isn't ideal, since it could also handle
the string allocations. So, instead of creating a fresh string, one can
simply call `alloc.as_string(format_args!(...))` and delegate the
allocation to the `DocAllocator` without any loss in expressivity. So,
in order to encorage this pattern, this commit also introduces the
`text!` macro.
In order to find all instances of the code pattern, the following
tree-sitter query was used:
```scm
(call_expression
function: (field_expression
field: (field_identifier) @field.name
(#eq? @field.name "text"))
arguments: (arguments
(macro_invocation
macro: (identifier) @macro.name
(#eq? @macro.name "format")))) @reference.call
```
At times we can have alias arguments that are recursive in their
position, but whose recursiveness is not immediately visible in the real
var.
Closes#5330
The algorithm for solving recursive definitions proceeds in several
steps. There are three main phases: introduction of what's known,
solving what's not known, and then checking our work of what was
inferred against what the programmer claimed. Concretely:
1. All explicitly-annotated signatures in the mutually recursive set are
introduced and let-generalized.
2. Then, inference type variables (`_`) and unannotated def signatures are
introduced to the cycle, without generalization. The bodies of these
defs, that are either unannotated or have inference variables, are
solved.
3. The defs from step (2) are now let-generalized, since we now know
that their types are consistent. At this point, all the defs in the
cycle have their types introduced and let-generalized, but we still
haven't checked the bodies of the defs froom step (1).
4. Check the bodies of explicitly-annotated defs in recursive set. This
might materially affect the actual types in the signature, for
example do to fixpoint-fixing or alias expansion.
5. As a result of (4) possibly changing the structure of the annotated
type, and because the previous annotated types in (1) were introduced
at a lower rank, we now re-introduce and re-generalize the solved def
types, in the same we did in step (3).
5. The rest of the program is solved.
Now, a very important thing here is that the annotation signature
introduced for (1) consists of different type variables than the
annotation signature introduced in (5). The reason is that they live at
different ranks. Prior to this patch we were not explicilty doing so;
this commit ensures that we do.
When we have a tag union type, outside of special cases in the middle of
unification, its extension type should either be (1) the closed tag
union or (2) a flex/rigid var. This adds an assertion for that.
We must be careful to ensure that if unifying nested lambda sets
results in disjoint lambdas, that the parent lambda sets are
ultimately treated disjointly as well.
Consider
```
v1: {} -[ foo ({} -[ bar Str ]-> {}) ]-> {}
~ v2: {} -[ foo ({} -[ bar U64 ]-> {}) ]-> {}
```
When considering unification of the nested sets
```
[ bar Str ]
~ [ bar U64 ]
```
we should not unify these sets, even disjointly, because that would
ultimately lead us to unifying
```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str, bar U64 ]-> {}) ] -> {}
```
which is quite wrong - we do not have a lambda `foo` that captures
either `bar captures: Str` or `bar captures: U64`, we have two
different lambdas `foo` that capture different `bars`. The target
unification is
```
v1 ~ v2
=> {} -[ foo ({} -[ bar Str ]-> {}),
foo ({} -[ bar U64 ]-> {}) ] -> {}
```
Closes#4712
