These tests fail currently because we have not implemented type
reconstruction in the presence of annonation-only declarations, but it's
good to keep track of them for later.
This is mostly the same as the procedure for unannotated `FunctionDef`s.
The only differences are that we need to
1. note the rigid type variables that are a part of the FunctionDef
2. generate fresh type variables for the function arguments, and
constrain them to the types of the arguments passed to us in the
annotation
This is enough to get the constraint generation working. There are more
interesting cases that properly typecheck in the main compiler but do
not typecheck given the current state of the editor AST (see the second
test in this commit), but this is a bug due to canonicalization, not
type reconstruction.
We ened to store the mapping of `rigid type vars -> user-declared names`
for presentation later on when we reconstruct the type of an expression
and want to pretty-print it for the user. This information is most
naturally captured on `output.introduced_variables`, as the main
compiler does so there.
We don't currently record this mapping while translating `Annotation`s
to `Annotation2`s (though we could), so we store it when we hit an
annotated expression that now needs to become an `Expr2`.
Moving from storing these as slices to `Lowercase`s makes it easier to
transform to shapes we'll need later during type reconstruction, for
example a mapping of rigid type variables to their lowercase variable
names.
Rigid vars are added to types after solutions are already found and are
only relevant for pretty printing elaborated types, so we don't keep
track of/care about their rigid names until the end of solution.
Previously we didn't provide this information in tests, though - now we
do.
The size of a `(PatternId, Type2)` tuple is 40 bytes (4 for the
`PatternId`, 4 bytes padding, 32 for the `Type2`). This doesn't fit in
an item slot allocated by the pool, which has a max of 32 bytes. So, we
allocate the Type2 itself on the pool, and then reference its pool ID in
the resulting tuple, which lowers the total size of the tuple to 8
bytes. This is a bit wasteful, but I couldn't find a better solution
without significantly more rework.
We also reorder the Type2 and PatternId fields in the tuple to better
align with the typical `(type|type variable, pattern|expression)` tuple
structure that exists in e.g. `FunctionDef::NoAnnotation`.
We do this by treating function definition bodies as equivalent to
closures, and piggy-backing on existing work to generate constraints
over closures. Then, we just bind the function name with the resolved
type of the function body.
Support for constraint generation in the presence of annotated functions
will be added later.
Prior to this patch we would not explicitly name solved type variables,
causing the elaborated type to appear unconstrained even when the
internal representation was constrained. For example, given a definition
like
```
\a, b -> Pair a b
```
we would generate distinct, fresh type variables for `a` and `b` but not
name them after solution. So even though the compiler knows they are
distinct, printing to the surface syntax would emit
```
*, * -> [ Pair * * ]*
```
which is incorrect, as the result type is constrained on the input type.
Instead, we now properly emit
```
a, b -> [ Pair a b ]*
```
naming variables where dependencies do exist. Where type variables are
don't constrain anything else, we can and do continue to emit the
wildcard type.