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

@@ -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()
-            }
+            },
         ])
     );
 }

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((

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); }
                         }
                     }