From 2c288dbff326f6af7a3e1624b3edc3d8f764f5d6 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 12 Mar 2025 16:38:39 +0100
Subject: [PATCH 1/4] fix tests

- in subtype unification: correctly propagate error
- in case of subtype between two ladders, check that the matching sub-ladders end at the same bottom rung (to exclude trait-types from sub-types)
---
 src/test/morphism.rs    | 14 ++++++++++----
 src/test/unification.rs |  2 +-
 src/unification.rs      | 15 ++++++++++++---
 3 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index 294ac00..fc0419a 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -419,6 +419,12 @@ fn test_morphism_path_listedit()
             dst_type: dict.parse("Char ~ EditTree").unwrap()
         })
     );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List~Vec Char>").unwrap(),
+            dst_type: dict.parse("<List Char>").unwrap()
+        })
+    );
     base.add_morphism(
         DummyMorphism(MorphismType{
             src_type: dict.parse("<List Char>").unwrap(),
@@ -483,12 +489,12 @@ fn test_morphism_path_listedit()
             },
             MorphismInstance {
                 m: DummyMorphism(MorphismType{
-                    src_type: dict.parse("<List~Vec ReprTree>").unwrap(),
-                    dst_type: dict.parse("<List ReprTree> ~ EditTree").unwrap()
+                    src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(),
+                    dst_type: dict.parse("<List Char> ~ EditTree").unwrap()
                 }),
-                halo: dict.parse("<Seq~List <Digit 10>~Char>").unwrap(),
+                halo: dict.parse("<Seq~List <Digit 10>>").unwrap(),
                 σ: HashMap::new()
-            }
+            },
         ])
     );
 }
diff --git a/src/test/unification.rs b/src/test/unification.rs
index de31d5b..dfff9d2 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -142,7 +142,7 @@ fn test_subtype_unification() {
 
     assert_eq!(
         UnificationProblem::new_sub(vec![
-            (dict.parse("<Seq~T <Digit 10> ~ Char>").unwrap(),
+            (dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(),
                 dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()),
         ]).solve(),
         Ok((
diff --git a/src/unification.rs b/src/unification.rs
index eb55646..5fb0818 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -255,6 +255,7 @@ impl UnificationProblem {
                         halo: TypeTerm::unit(),
                         addr: new_addr
                     }) {
+                        if a1.len() == i+a2.len() {
                         for j in 0..a2.len() {
                             if i+j < a1.len() {
                                 let mut new_addr = unification_pair.addr.clone();
@@ -283,6 +284,13 @@ impl UnificationProblem {
                             } else {
                                 TypeTerm::Ladder(halo).strip()
                             });
+                        } else {
+                            /* after the first match, the remaining ladders dont have the same length
+                             * thus it cannot be a subtype,
+                             * at most it could be a trait type
+                             */
+                        }
+
                     } else {
                         halo.push(a1[i].clone());
                         //eprintln!("could not unify ladders");
@@ -339,7 +347,7 @@ impl UnificationProblem {
 //                        eprintln!("after strip: {:?}", y);
 //                        eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
 
-                        if let Ok(halo) = self.eval_subtype(
+                        match self.eval_subtype(
                             UnificationPair {
                                 lhs: x.clone(),
                                 rhs: y.clone(),
@@ -347,6 +355,7 @@ impl UnificationProblem {
                                 addr: new_addr,
                             }
                         ) {
+                            Ok(halo) => {
                             if halo == TypeTerm::unit() {
                                 let mut y = y.clone();
                                 y.apply_substitution(&|k| self.σ.get(k).cloned());
@@ -376,8 +385,8 @@ impl UnificationProblem {
                                 halo_args.push(halo);
                                 n_halos_required += 1;
                             }
-                        } else {
-                            return Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
+                            },
+                            Err(err) => { return Err(err); }
                         }
                     }
 

From fe73c47504c63bd7db9dc3a50f3595600a00e6bb Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 14 Mar 2025 17:44:27 +0100
Subject: [PATCH 2/4] find_morphism_path(): param-normalize halo

---
 src/morphism.rs      | 10 ++++----
 src/test/morphism.rs | 59 ++++++++------------------------------------
 2 files changed, 15 insertions(+), 54 deletions(-)

diff --git a/src/morphism.rs b/src/morphism.rs
index 7b2ac5e..9f29ba8 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -21,8 +21,8 @@ pub struct MorphismType {
 impl MorphismType {
     pub fn normalize(self) -> Self {
         MorphismType {
-            src_type: self.src_type.normalize().param_normalize(),
-            dst_type: self.dst_type.normalize().param_normalize(),
+            src_type: self.src_type.strip().param_normalize(),
+            dst_type: self.dst_type.strip().param_normalize(),
 /*
             subtype_bounds: Vec::new(),
             trait_bounds: Vec::new()
@@ -149,7 +149,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
                     if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
                         dst_types.push(
                             MorphismInstance {
-                                halo: TypeTerm::Ladder(dst_halo_ladder).normalize(),
+                                halo: TypeTerm::Ladder(dst_halo_ladder).strip().param_normalize(),
                                 m: map_morph,
                                 σ: item_morph_inst.σ
                             }
@@ -221,7 +221,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
 
                         n.halo = n.halo.clone().apply_substitution(
                             &|k| σ.get(k).cloned()
-                        ).clone().strip();
+                        ).clone().strip().param_normalize();
 
                         n.σ = new_σ;
                     }
@@ -256,7 +256,7 @@ impl<M: Morphism + Clone> MorphismBase<M> {
 
                         n.halo = n.halo.clone().apply_substitution(
                             &|k| next_morph_inst.σ.get(k).cloned()
-                        ).clone().strip();
+                        ).clone().strip().param_normalize();
 
                         n.σ = new_σ;
                     }
diff --git a/src/test/morphism.rs b/src/test/morphism.rs
index fc0419a..e6db4a3 100644
--- a/src/test/morphism.rs
+++ b/src/test/morphism.rs
@@ -330,51 +330,6 @@ fn test_morphism_path_posint() {
             ]
         )
     );
-
-
-
-/*
-    assert_eq!(
-        base.find_morphism_path(MorphismType {
-            src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-            dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap()
-        }),
-        Some(
-            vec![
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(),
-                dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(),
-            ]
-        )
-    );
-    */
-/*
-    assert_eq!(
-        base.find_morphism_with_subtyping(
-            &MorphismType {
-                src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
-                dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-            }
-        ),
-
-        Some((
-                DummyMorphism(MorphismType{
-                    src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
-                    dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
-                }),
-
-                dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>>").unwrap(),
-
-                vec![
-                    (dict.get_typeid(&"Radix".into()).unwrap(),
-                    dict.parse("10").unwrap())
-                ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>()
-        ))
-    );
-*/
 }
 
 #[test]
@@ -421,14 +376,20 @@ fn test_morphism_path_listedit()
     );
     base.add_morphism(
         DummyMorphism(MorphismType{
-            src_type: dict.parse("<List~Vec Char>").unwrap(),
-            dst_type: dict.parse("<List Char>").unwrap()
+            src_type: dict.parse("Char").unwrap(),
+            dst_type: dict.parse("Char ~ ReprTree").unwrap()
         })
     );
     base.add_morphism(
         DummyMorphism(MorphismType{
-            src_type: dict.parse("<List Char>").unwrap(),
-            dst_type: dict.parse("<List Char~ReprTree>").unwrap()
+            src_type: dict.parse("Char ~ ReprTree").unwrap(),
+            dst_type: dict.parse("Char").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<List~Vec Char>").unwrap(),
+            dst_type: dict.parse("<List Char>").unwrap()
         })
     );
     base.add_morphism(

From dc6626833d771b8bc377ac34f4fe8d79291fc224 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Fri, 14 Mar 2025 17:46:59 +0100
Subject: [PATCH 3/4] add failing unification testcase

---
 src/test/unification.rs | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/test/unification.rs b/src/test/unification.rs
index dfff9d2..6480b13 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -251,6 +251,26 @@ fn test_trait_not_subtype() {
     );
 }
 
+#[test]
+fn test_reprtree_list_subtype() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname("Item".into());
+
+    assert_eq!(
+        subtype_unify(
+            &dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect(""),
+            &dict.parse("<List~Vec Item~ReprTree>").expect("")
+        ),
+        Ok((
+            TypeTerm::unit(),
+            vec![
+                (dict.get_typeid(&"Item".into()).unwrap(), dict.parse("<Digit 10>~Char").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}
+
 #[test]
 pub fn test_subtype_delim() {
     let mut dict = BimapTypeDict::new();

From 3eaca0dc376b7be2c0e803419a7d07203de50416 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 15 Mar 2025 11:33:48 +0100
Subject: [PATCH 4/4] work on unification

- add more unification tests
- rewrite subtype unification of ladders to work from bottom up
---
 src/test/unification.rs |  68 ++++++++--
 src/unification.rs      | 269 ++++++++++++++++++++++++----------------
 2 files changed, 224 insertions(+), 113 deletions(-)

diff --git a/src/test/unification.rs b/src/test/unification.rs
index 6480b13..6021dda 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -132,7 +132,61 @@ fn test_unification() {
 }
 
 #[test]
-fn test_subtype_unification() {
+fn test_subtype_unification1() {
+    let mut dict = BimapTypeDict::new();
+    dict.add_varname(String::from("T"));
+
+    assert_eq!(
+        UnificationProblem::new_sub(vec![
+            (dict.parse("A ~ B").unwrap(),
+                dict.parse("B").unwrap()),
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A").unwrap() ],
+            vec![].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        UnificationProblem::new_sub(vec![
+            (dict.parse("A ~ B ~ C ~ D").unwrap(),
+                dict.parse("C ~ D").unwrap()),
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A ~ B").unwrap() ],
+            vec![].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        UnificationProblem::new_sub(vec![
+            (dict.parse("A ~ B ~ C ~ D").unwrap(),
+                dict.parse("T ~ D").unwrap()),
+        ]).solve(),
+        Ok((
+            vec![ TypeTerm::unit() ],
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("A ~ B ~ C").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+
+    assert_eq!(
+        UnificationProblem::new_sub(vec![
+            (dict.parse("A ~ B ~ C ~ D").unwrap(),
+                dict.parse("B ~ T ~ D").unwrap()),
+        ]).solve(),
+        Ok((
+            vec![ dict.parse("A").unwrap() ],
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("C").unwrap())
+            ].into_iter().collect()
+        ))
+    );
+}
+
+#[test]
+fn test_subtype_unification2() {
     let mut dict = BimapTypeDict::new();
 
     dict.add_varname(String::from("T"));
@@ -232,9 +286,9 @@ fn test_trait_not_subtype() {
             &dict.parse("A ~ B ~ C").expect("")
         ),
         Err(UnificationError {
-            addr: vec![],
-            t1: dict.parse("A ~ B").expect(""),
-            t2: dict.parse("A ~ B ~ C").expect("")
+            addr: vec![1],
+            t1: dict.parse("B").expect(""),
+            t2: dict.parse("C").expect("")
         })
     );
 
@@ -244,9 +298,9 @@ fn test_trait_not_subtype() {
             &dict.parse("<Seq~List~Vec Char~ReprTree>").expect("")
         ),
         Err(UnificationError {
-            addr: vec![1],
-            t1: dict.parse("<Digit 10> ~ Char").expect(""),
-            t2: dict.parse("Char ~ ReprTree").expect("")
+            addr: vec![1,1],
+            t1: dict.parse("Char").expect(""),
+            t2: dict.parse("ReprTree").expect("")
         })
     );
 }
diff --git a/src/unification.rs b/src/unification.rs
index 5fb0818..767bbde 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -137,85 +137,119 @@ impl UnificationProblem {
         }
     }
 
+
+
+    pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> {
+
+        if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) {
+            return Ok(());
+        }
+
+        if new_lower_bound.contains_var(v) {
+            // loop
+            return Err(());
+        }
+
+        if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
+//                        eprintln!("var already exists. check max. type");
+            if let Ok(halo) = self.eval_subtype(
+                UnificationPair {
+                    lhs: lower_bound.clone(),
+                    rhs: new_lower_bound.clone(),
+                    halo: TypeTerm::unit(),
+                    addr: vec![]
+                }
+            ) {
+//                            eprintln!("found more general lower bound");
+//                            eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+                // generalize variable type to supertype
+                self.lower_bounds.insert(v, new_lower_bound);
+                Ok(())
+            } else if let Ok(halo) = self.eval_subtype(
+                UnificationPair{
+                    lhs: new_lower_bound,
+                    rhs: lower_bound,
+                    halo: TypeTerm::unit(),
+                    addr: vec![]
+                }
+            ) {
+//                            eprintln!("OK, is already larger type");
+                 Ok(())
+            } else {
+//                            eprintln!("violated subtype restriction");
+                Err(())
+            }
+        } else {
+//                        eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+            self.lower_bounds.insert(v, new_lower_bound);
+            Ok(())
+        }
+    }
+
+
+    pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> {
+        if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) {
+            return Ok(());
+        }
+
+        if new_upper_bound.contains_var(v) {
+            // loop
+            return Err(());
+        }
+
+        if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
+            if let Ok(_halo) = self.eval_subtype(
+                UnificationPair {
+                    lhs: new_upper_bound.clone(),
+                    rhs: upper_bound,
+                    halo: TypeTerm::unit(),
+                    addr: vec![]
+                }
+            ) {
+                // found a lower upper bound
+                self.upper_bounds.insert(v, new_upper_bound);
+                Ok(())
+            } else {
+                Err(())
+            }
+        } else {
+            self.upper_bounds.insert(v, new_upper_bound);
+            Ok(())
+        }
+    }
+
     pub fn eval_subtype(&mut self, unification_pair: UnificationPair) -> Result<
         // ok: halo type
         TypeTerm,
         // error
         UnificationError
     > {
+        eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
         match (unification_pair.lhs.clone(), unification_pair.rhs.clone()) {
 
             /*
              Variables
             */
 
-            (t, TypeTerm::TypeID(TypeID::Var(varid))) => {
-//                eprintln!("t <= variable");
-                if ! t.contains_var( varid ) {
-                   // let x = self.σ.get(&TypeID::Var(varid)).cloned();
-                    if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() {
-//                        eprintln!("var already exists. check max. type");
-                        if let Ok(halo) = self.eval_subtype(
-                            UnificationPair {
-                                lhs: lower_bound.clone(),
-                                rhs: t.clone(),
-                                halo: TypeTerm::unit(),
-                                addr: vec![]
-                            }
-                        ) {
-//                            eprintln!("found more general lower bound");
-//                            eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
-                            // generalize variable type to supertype
-                            self.lower_bounds.insert(varid, t.clone());
-                        } else if let Ok(halo) = self.eval_subtype(
-                            UnificationPair{
-                                lhs: t.clone(),
-                                rhs: lower_bound.clone(),
-                                halo: TypeTerm::unit(),
-                                addr: vec![]
-                            }
-                        ) {
-//                            eprintln!("OK, is already larger type");
-                        } else {
-//                            eprintln!("violated subtype restriction");
-                            return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t });
-                        }
-                    } else {
-//                        eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
-                        self.lower_bounds.insert(varid, t.clone());
-                    }
-                    self.reapply_subst();
-                    Ok(TypeTerm::unit())
-                } else if t == TypeTerm::TypeID(TypeID::Var(varid)) {
+            (t, TypeTerm::TypeID(TypeID::Var(v))) => {
+                //eprintln!("t <= variable");
+                if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
                     Ok(TypeTerm::unit())
                 } else {
-                    Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t })
+                    Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
                 }
             }
 
-            (TypeTerm::TypeID(TypeID::Var(varid)), t) => {
-//                eprintln!("variable <= t");
-
-                if let Some(upper_bound) = self.upper_bounds.get(&varid).cloned() {
-                    if let Ok(_halo) = self.eval_subtype(
-                        UnificationPair {
-                            lhs: t.clone(),
-                            rhs: upper_bound,
-                            halo: TypeTerm::unit(),
-                            addr: vec![]
-                        }
-                    ) {
-                        // found a lower upper bound
-                        self.upper_bounds.insert(varid, t);
-                    }
+            (TypeTerm::TypeID(TypeID::Var(v)), t) => {
+                //eprintln!("variable <= t");
+                if self.add_upper_subtype_bound(v, t.clone()).is_ok() {
+                    Ok(TypeTerm::unit())
                 } else {
-                    self.upper_bounds.insert(varid, t);
+                    Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t })
                 }
-                Ok(TypeTerm::unit())
             }
 
 
-
             /*
              Atoms
             */
@@ -236,68 +270,91 @@ impl UnificationProblem {
             */
 
             (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => {
-                let mut halo = Vec::new();
-                if a1.len() < a2.len() {
-                    return Err(UnificationError {
-                        addr: vec![],
-                        t1: unification_pair.lhs,
-                        t2: unification_pair.rhs
-                    });
-                }
 
-                for i in 0..a1.len() {
-                    let mut new_addr = unification_pair.addr.clone();
-                    new_addr.push(i);
-                    if let Ok(r_halo) = self.eval_subtype( UnificationPair {
-                        lhs: a1[i].clone(),
-                        rhs: a2[0].clone(),
+                let mut l1_iter = a1.into_iter().enumerate().rev();
+                let mut l2_iter = a2.into_iter().rev();
 
-                        halo: TypeTerm::unit(),
-                        addr: new_addr
-                    }) {
-                        if a1.len() == i+a2.len() {
-                        for j in 0..a2.len() {
-                            if i+j < a1.len() {
-                                let mut new_addr = unification_pair.addr.clone();
-                                new_addr.push(i+j);
+                let mut halo_ladder = Vec::new();
 
-                                let lhs = a1[i+j].clone();//.apply_substitution(&|k| self.σ.get(k).cloned()).clone();
-                                let rhs = a2[j].clone();//.apply_substitution(&|k| self.σ.get(k).cloned()).clone();
+                while let Some(rhs) = l2_iter.next() {
+                    //eprintln!("take rhs = {:?}", rhs);
+                    if let Some((i, lhs)) = l1_iter.next() {
+                        //eprintln!("take lhs ({}) = {:?}", i, lhs);
+                        let mut addr = unification_pair.addr.clone();
+                        addr.push(i);
+                        //eprintln!("addr = {:?}", addr);
 
-                                if let Ok(rung_halo) = self.eval_subtype(
+                        match (lhs.clone(), rhs.clone()) {
+                            (t, TypeTerm::TypeID(TypeID::Var(v))) => {
+
+                                if self.add_upper_subtype_bound(v,t.clone()).is_ok() {
+                                    let mut new_upper_bound_ladder = vec![ t ];
+
+                                    if let Some(next_rhs) = l2_iter.next() {
+
+                                        // TODO
+
+                                    } else {
+                                        // take everything
+
+                                        while let Some((i,t)) = l1_iter.next() {
+                                            new_upper_bound_ladder.push(t);
+                                        }
+                                    }
+
+                                    new_upper_bound_ladder.reverse();
+                                    if self.add_upper_subtype_bound(v, TypeTerm::Ladder(new_upper_bound_ladder)).is_ok() {
+                                        // ok
+                                    } else {
+                                        return Err(UnificationError {
+                                            addr,
+                                            t1: lhs,
+                                            t2: rhs
+                                        });
+                                    }
+                                } else {
+                                    return Err(UnificationError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
+                                }
+                            }
+                            (lhs, rhs) => {
+                                if let Ok(ψ) = self.eval_subtype(
                                     UnificationPair {
                                         lhs: lhs.clone(), rhs: rhs.clone(),
-                                        addr: new_addr.clone(),
-                                        halo: TypeTerm::unit()
+                                        addr:addr.clone(), halo: TypeTerm::unit()
                                     }
                                 ) {
-                                    halo.push(rung_halo);
+                                    // ok.
+                                    //eprintln!("rungs are subtypes. continue");
+                                    halo_ladder.push(ψ);
                                 } else {
-                                    return Err(UnificationError{ addr: new_addr, t1: lhs, t2: rhs })
+                                    return Err(UnificationError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
                                 }
                             }
                         }
-
-                        return Ok(
-                            if halo.len() == 1 {
-                                halo.pop().unwrap()
-                            } else {
-                                TypeTerm::Ladder(halo).strip()
-                            });
-                        } else {
-                            /* after the first match, the remaining ladders dont have the same length
-                             * thus it cannot be a subtype,
-                             * at most it could be a trait type
-                             */
-                        }
-
                     } else {
-                        halo.push(a1[i].clone());
-                        //eprintln!("could not unify ladders");
+                        // not a subtype,
+                        return Err(UnificationError {
+                            addr: vec![],
+                            t1: unification_pair.lhs,
+                            t2: unification_pair.rhs
+                        });
                     }
                 }
+                //eprintln!("left ladder fully consumed");
 
-                Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                for (i,t) in l1_iter {
+                    halo_ladder.push(t);
+                }
+                halo_ladder.reverse();
+                Ok(TypeTerm::Ladder(halo_ladder).strip().param_normalize())
             },
 
             (t, TypeTerm::Ladder(a1)) => {
@@ -362,9 +419,9 @@ impl UnificationProblem {
                                 y = y.strip();
                                 let mut top = y.get_lnf_vec().first().unwrap().clone();
                                 halo_args.push(top.clone());
-//                                eprintln!("add top {:?}", top);
+                                //eprintln!("add top {:?}", top);
                             } else {
-//                                eprintln!("add halo {:?}", halo);
+                                //eprintln!("add halo {:?}", halo);
                                 if n_halos_required > 0 {
                                     let x = &mut halo_args[n_halos_required-1];
                                     if let TypeTerm::Ladder(argrs) = x {
@@ -391,7 +448,7 @@ impl UnificationProblem {
                     }
 
                     if n_halos_required > 0 {
-//                        eprintln!("halo args : {:?}", halo_args);
+                        //eprintln!("halo args : {:?}", halo_args);
                         Ok(TypeTerm::App(halo_args))
                     } else {
                         Ok(TypeTerm::unit())