Additional thoughts:

1. Once we implement sum types, unification (unifyTypes) will always result with a sum type if it can't find another way to unify types, right? So if it can't unify types T1 and T2 in any other way, it should unify them as T1 | T2 I think. In that case, there won't be any UnificationErrors anymore, right? Hmmmm, interesting. If so, this will potentially result in nicer error messages, since we won't have the "can't mix the following types" messages any more, instead it will be unexpected type error with actual type being a sum type, which offer more information (the expected type).
2. When unifying types, what happens when we try to unify sum type with another type? I think what we need to do in that case is try to unify that another type with every single type from the sum type, one by one. If we manage to unify it with one of those, we stop and replace that type in the sum type with unified type. If not, we add this another type to the sum type as a new option. This should work recursively and also if another type is also a sum type.

@sodic and I discussed how to implement sum types in Wasp, here are some conclusions:

1. When unifying two types, we should try to construct as specific type as possible (this is what other languages, like TypeScript, also do). Sometimes exceptions are made for ergonomical reasons (check this TypeScript example), but it is not yet obvious that any exceptions should be made in the current Wasp type system.
2. Currently, when unifying dicts in Wasp, we have special rules how to do it in regards with optional dict fields, but with sum types, we can remove this special logic and just do normal sum types unification -> this should work equally well and we have no special rules.
3. So, specifically, based on conclusions above, when unifying two dictionaries, result will always be the sum of those two dictionaries -> we will not go inside of them and do unification on level of the specific fields. So, if we have [{ a :: Int, b :: String }, { a :: Boo, b :: Bool }], we want unification to result with [ { a :: Int, b :: String } | { a :: Bool, b :: Bool } ], not [ { a :: Int | Bool, b :: String | Bool } ].

More thoughts:

• empty list -> we have a special "empty list" type, so we should consider that. Unifying it with a non-empty list should simply result in the type of non-empty list.
• unification algorithm -> we can just put all the types together and do "unique" on them. But then we need to see if we can further reduce that type -> specifically, if there are any subtypes, those should be merged into their super types. For example if we have empty list and non-empty list, empty list we can just kick out. That is probably it, I don't think we have any other subtypes (in our case dictionaries are not sub-types since we are having a nominal typing system!), but we should still keep this in mind.

To cover the use case from the issue's description (e.g., supporting both pages and routes for to fields in route declarations):

route OldLoginRoute { path: "/signup", to: LoginRoute }
route LoginRoute { path: "/signup", to: LoginPage }

It should be enough to make changes inside checkStmnt and weaken functions, without needing to touch type inference and unification. This is because users will never be using the possibilities of sum types directly. More precisely, the user will either specify a page or a route (or cause an error by specifying something else), and Wasp then has to make sure whatever they used is assignable to type page | route

More generally, our main goal is to never show unification errors to the user. Instead, we'll always construct a sum type and handle potential errors in the weakening phase as "Expected type X, got type Y". Let's say a user specifies a list value as [1, "2", 3, 4]. The compiler currently says something like Cannot unify types Number and String which is a bit confusing to the user. We want it to say Expected to get a list of Numbers, but got a list of Numbers and Strings.

Unification errors can currently only happen in lists. When encountering a list, we should find the most common supertype of all elements and infer that. Wasp will later check the inferred type against the required type.

To make this change possible, it should be enough to change the function unifyTypes. Instead of throwing an error when finding two uncoercable types, it should return their reduced sum type. More precisely, there are three possible cases:

1. When unifyTypes receives two equivalent types T, it should return the type T
2. When unifyTypes receives two different types T and U, it should return their reduced sum type T | U
3. When unifyTypes receives a a list, it should fold it with unifyTypes.

While researching, I stumbled upon the discovery that we are actually implementing union types (not sum types). The difference comes from something we've touched on several times in an unrelated context. There are two kinds of unions:

1. Untagged unions (most often called "union types") - this is what TypeScript has (e.g., number | string) and what we want to add to Wasp
2. Tagged unions (most often called "sum types") - This is what Haskell has (e.g., data Either a b = Left a | Right b)

In essence, a sum type is a union type with explicit labels. Here are several helpful resources on the subject:

• A Wikipedia article on tagged unions
• An easy-to-read blog post
• A Stack Overflow comment (but most answers and comments are worth reading

By the way, several answers/comments in the above SO thread give a great answer to the question "Why doesn't Haskell support untagged unions?" Spoiler: you were on the right track with the reasoning that there would be massive inferred unions all over the place, but there's more to it.

Thanks for sharing @sodic this is very interesting! Ok great, then let's call them union types!

Interesting regarding Haskell -> I read what you shared and besides certain technical reasons, I understood it mostly comes down to cost / benefit ratio. It would not bring enough to Haskell to be worth the complexity it would introduce. Which makes sense to me! In our case though, I think it could be a good cost / benefit ratio, what do you think?

Yes, it definitely makes sense for us. Haskell already has tagged unions, so they wouldn't be getting much out of adding untagged unions (i.e., tagged unions already cover most use cases).

Since Wasp doesn't yet support any kind of unions, our cost/benefit ratio is very favorable.

We won't "penetrate" into type constructors (e.g., dictionaries, tuples). For example:

// this is inferred as [{ to: Route } | { to: Page }]
[{ to: Route }, { to: Page}]

It should be assignable to its supertype [{ to: Route | Page }]. We will check this during the weakening phase.
TypeScript does the same thing (playground link):

type T = { to: number | boolean }[]

let x = [{to: 1}, { to: true }]

In this session we defined new unifyTypes function, and we started implementing makeReducedUnionType function, by using UnorderedSet!

Ones we make that work, next big step will be implementing an algorithm in weaken that will correctly weaken sum types.

Before that we will also probably want to take care of TODOs and write some tests.

There is also Evaluator -> we will need to add support for UnionTypes there at some point, and figure out how are they deduced from AppSpec.

We finished implementing makeReducedUnionType, we updated unify function to reflect the changes, and we updated places where unify is called.

Next step is updating the weaken function! It will be interesting figuring out what to do with Dict.

We started writing tests and should continue from inferExpr - Type checks a list of dictionaries that unify but have different types.

Summary:

• We decided it was OK for now to unify lists of dictionaries as union types (as opposed to inferring optionals)
• We decided that we should explicitly handle those cases in weaken because of the error messages
• We thought about assigning types to expressions in the AST and concluded that we most likely don't want to lose type information by assigning inferred supertypes to child nodes. For example, when unifying a list, we only want to assign the supertype to the list node, we don't want to weaken the types of iits elements.

We fixed some of the tests!
Next steps:

1. Write tests for unifyTypes, and simplify tests for unify based on that.
2. Fix weaken -> also write tests while doing it and get other tests passing (they are now failing because of how weaken incorrectly works.
3. Take care of more prominent TODOs, first one being not weakening typed expressions while doing unify, and another is figuring out the best way to structure UnionType (and ensure order in it and some other stuff).

Today we implemented tests for unifyTypes.

Next time: continue writing test for weaken, and then let's implement weaken. We also have a lot of TODOs sprinkled around.

We wrote tests for weaken: some of them testing dealing with dictionaries optional field, some testing super types. We didn't write all of them, but we did define all of them, so next time we should continue from there, filling in the remaining tests!

• Finished the tests for weaken, haven't started editing weaken yet: c5bcea3
• Removed the function unify and changed a portion of inferExprType to prevent it from weakening list element types: 3bc592f

Next step:

• Remove the tests for unify
• Update the tests for inferExprType to ensure we don't weaken list element expression types
• Refactor the weaken function. Make sure to apply the same non-weakening subexpression logic to weaken (if necessary, check line 257)

We removed unify and its tests.
We updated the tests for inferExprType to ensure we don't weaken list element expression types.
Next step is refactoring the weaken function! And then taking care of all the TODOs.

We started looking into weaken, to consider if we need it at all.

We traced where it is used, and found that its only place of usage is currently in checkStmt, where it is used on the typed expression of the declaration.

The question was, is this needed? Can we just skip this part and instead of doing the weakening, which updates the types in typed expression tree to match the wanted type, can we just check that typed expression is a sub-type of wanted declaration type and that is it, don't do any weakening? So effectively we would refactor weaken into isSuperType (or isSubType) and that would be it.

But, will that be a problem down the road then? Does Evaluator expect the typed expression in the declaration to match the declaration type, or can it just be its sub type?
We searched for declEvaluate and found that it says (in Wasp.Analyzer.TypeDefinitions.Class.IsDeclType) that it assumes the type of typed expression is indeed the same as declaration type, so that would mean that it can't be a subtype, instead it expects it to be exactly the same type.
That said, we weren't sure if that assumption is actually important in the Evaluator -> if nobody uses that assumption, we could try relaxing it to assuming it is a sub type, not the exactly same type.

Therefore we next looked into the Evaluator, specifically how evaluation is implemented -> does it use that assumption or not. One interesting file is Wasp.Analyzer.Evaluator.Evaluation.TypedExpr.Combinators -> the most basic evaluation logic is defined there. None of these seemed to care about the type vs subtype difference.

Then next we looked into Wasp.Analyzer.TypeDefinitions.TH.Decl, to see how are these combinators further composed. Interesting pieces of code there were data WaspKind, genWaspTypeAndEvaluationForHaskellType, genDictWaspTypeAndEvaluationForRecord, ... .
Here, it seemed as if type vs subtype thing might be an issue, but we didn't look deep enough into it to figure out how to go about it yet.
We should continue with his direction, figure out if we can modify evaluators so that they don't require that assumption of exact type match but instead be ok with subtypes, and if we can, then do so and drop weaken. If not, we just make sure that weaken works as it should. But we should be able to do so, I think.

What we did conclude though is that it might be a good idea to take a step back and start from the AppSpec side, implementing Union type there, via Either or via our Union or maybe even via any custom data that is sum type in Haskell. We are not yet sure though what is better, to use something like Either/Union, or to use custom data (which in that case will need to have data constructors that have a single type each and those types must all be distinct). Oh another tricky thing -> in any case, what if we define union type in AppSpec in such way that one of the types in union is a sub type of the other type in union? That is not a valid union then, right? We should detect that and not accept it.

To conclude, there are main two directions to chase:

1. Can we get rid of weaken and not weaken any typed expressions? Or at least weaken only the top level -> declarations? We should explore evaluators and try to adjust them to accomplish this.
2. Introducing "union" to the AppSpec, via Either/Union, and/or via custom data types that have correct shape, while also handling the possibility of "union" not being reduced in its definition in AppSpec which means we probably can't evaluate it.

We started working on a new branch (branched out from main): https://github.com/wasp-lang/wasp/tree/filip-martin-weaken. The main idea is to first simplify (or completely get rid of) weaken and its logic. That is what the new branch is for. It also gives us an isolated place to test out whether our simplification plan works with the evaluator (Martin explained most of our concerns in the previous comment).

After we simplify the type inference (by making sure we don't traverse the AST twice and lose type information by weakening subexpressions after unification), we'll create a new branch for adding union types.

We merged the PR that removes the weakening and instead introduces the explicit notion of subtypes! This will make this PR much simpler.

For this PR we discussed we should continue in the following way:

1. Check out latest main, where "weakening" PR got merged, and continue from it from scratch, picking up pieces of code from this PR.
2. Decide how are we describing union type in AppSpec: Either, Union, or custom sum data type. Make sure that it is fully reduced (check it).
3. The fact that we have isSubtypeOf should help us a lot. unifyTypes t1 t2 should come down to checking if t1 is subtype of t2 and vice versa, and if so, returns the super type of those two, otherwise it does union. This will take care of unifying unions, empty list, dicts, ... -> everything. Reduction of union type should also come down to checking for subtypes (quadratically?).