Introduce annotation in first step of recursive solving independently

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.
This commit is contained in:
Ayaz Hafiz 2023-04-10 15:54:45 -05:00
parent 352345d1d9
commit b9ab93fd98
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 113 additions and 54 deletions

View file

@ -0,0 +1,17 @@
app "test" provides [main] to "./platform"
main =
f = \x -> x + 1
map : { f1: (I64 -> I64) } -> List I64
map = \{ f1 } -> List.concat [f1 1] (map { f1 })
# ^^^ { f1 : I64 -[[]]-> I64 } -[[map(2)]]-> List I64
# ^^^ { f1 : I64 -[[]]-> I64 } -[[map(2)]]-> List I64
map { f1: f }
# ^^^{inst} { f1 : I64 -[[f(1)]]-> I64 } -[[map(2)]]-> List I64
# │ map : { f1: (I64 -> I64) } -> List I64
# │ map = \{ f1 } -> List.concat [f1 1] (map { f1 })
# │ ^^^ { f1 : I64 -[[f(1)]]-> I64 } -[[map(2)]]-> List I64
# │ ^^^ { f1 : I64 -[[f(1)]]-> I64 } -[[map(2)]]-> List I64