From 34fd8fa0a09da3000fdc6d02e726ab2e4b9a3c22 Mon Sep 17 00:00:00 2001
From: Alexander Nutz <alexander.nutz@vxcc.dev>
Date: Sat, 20 Sep 2025 12:41:58 +0200
Subject: [PATCH] untagged union types

---
 spec.md | 27 ++++++++++-----------------
 1 file changed, 10 insertions(+), 17 deletions(-)

diff --git a/spec.md b/spec.md
index 5e307d7..bcd33ec 100644
--- a/spec.md
+++ b/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