untagged union types

spec.md

@@ -14,7 +14,9 @@
 One of:
 - `t -> t`: pure function taking `t` as argument, and returning `t`
 - `{ field1: xt, field2: yt }`: non-nominal records
-- `'Case1 t | 'Case2 t2 | 'Case3 t3`: tagged unions
+- `'MyTag t`: tagged type. If `t` is already tagged, the old tag will be overwritten!
+  The type can be omitted, defaulting to `Unit`: `'Example` is identical to `Example Unit`
+- `t | t2 | t3`: un-tagged unions
 - `with myGenericName: x`: introduce "generic" type `myGenericName`, which can be used in type `x`
 - `&a 'EOL | 'Cons {v: t, next: a}`: [recursive type](##recursive-types)
 - `?Identifier`: the partial type `Identifier`
@@ -56,7 +58,7 @@ type Illegal2 = &a {x: a, y: Int8}
 
 The definition of "infinite size" is:
 - for records: if _any_ of the field types has "infinite size"
-- for unions: if _all_ of the cases has "infinite size"
+- for unions: if _all_ of the cases have "infinite size"
 - for functions: never
 - for recursive types:
   - if the type was already visited: yes
@@ -111,9 +113,10 @@ extend Plan with 'WritelnPlan Unit
 Check if type is compatible-with / assignable-to type requirements.
 
 - a type is compatible with itself ofcourse
-- a tagged union is compatible with anothr,
+- a (un-tagged) union is compatible with anothr,
   if the other one contains at least all cases from this union,
-  and those cases are compatible
+  determined by weather or not thos are compatible
+- a `'Tag t` is compatible with `t`, or `'Tag t`, but NOT `'OtherTag t`
 - a non-nominal record is compatbile with anohter,
   if the other one contains a _subset_ of the fields of this one,
   and the field types are comptible.
@@ -129,19 +132,9 @@ TODO: need more details?
 This process is performed on the resulting types of two merging branches
 
 Tries, in order:
-- if one of the types is a tagged union,
-  which contains only one case with an identical type,
-  and the other is not a tagged union,
-  it will "attach" that case onto the other type, like this:
-  `'N Num | 'I Int` and `Num` -> `'N Num | 'I Int`
-- if one of the types is a tagged union with exactly one case,
-  and the other one is not an union,
-  it will put that tag onto it, and phi-merge the inner types.
-  example: `'N Num` and `Num` -> `'N Num`
-- if both types are tagged unions,
-  the result is an tagged union contain the csaes of both tagged unions.
-  union cases that are in both branches, will have their types phi-unified too.
-  example: `'Ok ('N Num | 'I Int) | 'SomeErr` and `'Ok Num | 'AnotherErr` -> `'Ok ('N Num) | 'SomeErr | 'AnotherErr`
+- if one of them is `'Tag a`, and the other is `b` (tagless!), will unify to `'Tag PHI(a,b)`
+- if one of them is a union, and the other one is a `t`,
+  it will first try for each case to unify `t` with the case, and otherwise create a new case of `t`
 - if both types are non-nominal records,
   the result will contain only fields that are present in both types.
   The types of the fields will get phi-unified too