At the time we introduced presence constraints for tag unions, I added a
"destruct_position" variable so that we didn't change the typechecking
semantics for everything all at once, and because I wasn't totally sure
what I was doing was correct. But now we're more confident in this
approach, and every pattern is by definition a destructuring, so there
is no need for this flag.
Also should fix some potential bugs we didn't notice before with presence
constraints in closure variables, though I can't find a good test to
reproduce this, since closure variables are hidden from the user.
I was hoping to add nested datatypes into the language, but it turns out
doing so is quite tricky and not all that useful with Roc's current
compilation model. Basically every implementation strategy I could think
of ended up requiring a uniform representation for the data layout
(or some ugly workaround). Furhermore it increased the complexity of the
checker/mono IR generator a little bit - basically, we must always pass
around the alias definitions of nested datatypes and instantiate them
at usage sites, rather than being able to unroll aliases as we currently
do during canonicalization.
So, especially because we don't support polymorphic recursion anyway, I
think it may be better to simply disallow any kind of nested datatypes
in the language. In any case, Stephanie Weirich [seems to think nested
datatypes are not needed](https://www.cis.upenn.edu/~plclub/blog/2020-12-04-nested-datatypes/).
Closes#2293
This code has a shadowing error:
```
b = False
f = \b -> b
f b
```
but prior to this commit, the compiler would hit an internal error
during monomorphization and not even get to report the error. The reason
was that when we entered the closure `\b -> b`, we would try to
introduce the identifier `b` to the scope, see that it shadows an
existing identifier, and not insert the identifier. But this meant that
when checking the body of `\b -> b`, we would think that we captured the
value `b` in the outer scope, but that's incorrect!
The present patch fixes the issue by generating new symbols for
shadowing identifiers, so deeper scopes pick up the correct reference.
This also means in the future we may be able to compile and execute code
with shadows, even though it will still be an error.
Closes#2343
This work is related to restricting tag union sizes in input positions.
As an example, for something like
```
\x -> when x is
A M -> X
A N -> X
A _ -> X
```
we'd like to infer `[A [M, N]* ]` rather than the `[A, [M, N]* ]*` we
infer today. Notice the difference is that the former type tells us we
only accepts `A`s, but the argument of the `A` can be `M`, `N` or
anything else (hence the `_`).
So what's the idea? It's an encoding of the "must have"/"might have"
design discussed in https://github.com/rtfeldman/roc/issues/1758. Let's
take our example above and walk through unification of each branch.
Suppose `x` starts off as a flex var `t`.
```
\x -> when x is
A M -> X
```
Now we introduce a new kind of constraint called a "presence"
constraint. It says "t has at least [A [M]]". I'll notate this as `t +=
[A [M]]`. When `t` is free as it is here, this is equivalent to `t ~
[A [M]]`.
```
\x -> when x is
...
A N -> X
```
At this branch we introduce the presence constraint `[A [M]] += [A [N]]`.
Notice that there's two tag unions we care about resolving here - one is
the toplevel one that says "I have an `A ...` inside of me", and the
other one is the tag union that's the tyarg to `A`. They are distinct
and at different depths.
For the toplevel one, we first figure out if the number of tags in the
union needs to expand. It does not - we're hoping to resolve the type
`[A [M, N]]`, which only has `A` in the toplevel union. So, we don't
need to do anything extra there, other than the merge the nested tag
unions.
We recurse on the shared tags, and now we have the presence constraint
`[M] += [N]`. At this point it's important to remember that the left and
right hand types are backed by type variables, so this is really
something like `t11 [M] += t12 [N]`, where `[M]` and `[N]` are just what
we know the variables `t11` and `t12` to be at this moment. So how do we
solve for `t11 [M, N]` from here? Well, we can encode this constraint as
a type variable definition and a unification constraint we already know
how to solve:
```
New definition: t11 [M]a (a fresh)
New constraint: a ~ t12 [N]
```
That's it; upon unification, `t11 [M, N]` falls out.
Okay, last step.
```
\x -> when x is
...
A _ -> X
```
We now have `[A [M, N]] += [A a]`, where `a` is a fresh unbound
variable. Again nothing has to happen on the toplevel. We walk down and
find `t11 [M, N] += t21 a`. This is actually called an "open constraint"; we
differentiate it at the time we generate constraints because it follows
syntactically from the presence of an `_`, but it's semantically
equivalent to the presence constraint `t11 [M, N] += t21 a`. It's just
called opening because literally the only way `t11 [M, N] += t21 a` can
be true is if we set `t11 a`. Well, actually, we assume `a` is a tag
union, so we just make `t11` the open tag union `[M, N]a`. Since `a` is
unbound, this eventually becomes a wildcard and hence falls out `[M, N]*`.
Also, once we open a tag union with an open constraint, we never close
it again.
That's it. The rest falls out recursively. This gives us a really easy
way to encode these ordering constraints in the unification-based system
we have today with minimal additional intervention. We do have to patch
variables in-place sometimes, and the additive nature of these
constraints feels about out-of-place relative to unification, but it
seems to work well.
Resolves#1758
This reverts commit 6e4fd5f06a1ae6138659b0073b4e2b375a499588.
This idea didn't work out because cloning the type and storing it on a
variable still resulted in the solver trying to uify the variable with
the type. When there were errors, which there certainly would be if we
tried to unify the variable with a structure that had nested flex/rigid
vars, the nested flex/rigid vars would inherit those errors, and the
program wouldn't typecheck.
Since the motivation here was to expose the signature type to
`reporting` so that we could modify it with suggestions, we should
instead pass that information along in something analogous to the
`Expected` struct.
To provide better error messages and suggestions related to changing
type annotations, we now pass annotation type signatures all the way
down through the constraint solver. At constraint generation we
associate the type signature with a unique variable, and during error
reporting, we pull out an `ErrorType` corresponding to the original type
signature, by looking up the unique variable. This gives us two nice
things:
1. It means we don't have to pass the original, AST-like type
annotation, which can be quite large, to everyone who looks at an
expectation.
2. It gives us a translation from a `Type` to an `ErrorType` for free
using the existing translation procedure in `roc_types::subs`,
without having to create a new translation function.
This makes it easier for error reporting to find the relevant
annotations that were part of a type error, and display that in the
error message presented to a user.
Previously, a program like
```roc
word = "word"
if True then 1 else "\(word) is a word"
```
would report an error like
```
── TYPE MISMATCH ───────────────────────────────────────────────────────────────
This `if` has an `else` branch with a different type from its `then` branch:
3│ if True then 1 else "\(word) is a word"
^^^^^^^^^^^^^^^^^^
This concat all produces:
Str
but the `then` branch has the type:
Num a
I need all branches in an `if` to have the same type!
```
but this is a little bit confusing, since the user shouldn't have to
know (or care) that string interpolations are equivalent to
concatenations under the current implementation.
Indeed we should make this fully transparent. We now word the error
message by taking into account the way calls are made. To support the
case shown above, we introduce the `CalledVia::Sugar` variant to
represent the fact that some calls may be the result of desugaring the
surface syntax.
This commit also demonstrates the usage of `CalledVia` to produce better
error messages where we use binary comparison operators like `<`. There
are more improvements we can make here for all `CalledVia` variants, but
this is a good starting point to demonstrate the usage of the new
procedure.
Closes#1714
