rewrite enum_morphisms & find_morphism_path

- introduce `MorphismInstantiation` which instantiates a
  morphism-template using a type-substitution and a halo type.
- find_morphism_path returns list of `MorphismInstatiation`.

src/lib.rs

@@ -11,6 +11,7 @@ pub mod lnf;
 pub mod pnf;
 pub mod subtype;
 pub mod unification;
+pub mod morphism;
 
 #[cfg(test)]
 mod test;
@@ -23,4 +24,5 @@ pub use {
     term::*,
     sugar::*,
     unification::*,
+    morphism::*
 };

src/morphism.rs

@@ -0,0 +1,343 @@
+use {
+    crate::{
+        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
+    },
+    std::{collections::HashMap, u64}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct MorphismType {
+    pub src_type: TypeTerm,
+    pub dst_type: TypeTerm,
+}
+
+impl MorphismType {
+    pub fn normalize(self) -> Self {
+        MorphismType {
+            src_type: self.src_type.normalize().param_normalize(),
+            dst_type: self.dst_type.normalize().param_normalize()
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub trait Morphism : Sized {
+    fn get_type(&self) -> MorphismType;
+    fn map_morphism(&self, seq_type: TypeTerm) -> Option< Self >;
+
+    fn weight(&self) -> u64 {
+        1
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq)]
+pub struct MorphismInstance<M: Morphism + Clone> {
+    pub halo: TypeTerm,
+    pub m: M,
+    pub σ: HashMap<TypeID, TypeTerm>
+}
+
+impl<M: Morphism + Clone> MorphismInstance<M> {
+    pub fn get_type(&self) -> MorphismType {
+        MorphismType {
+            src_type: TypeTerm::Ladder(vec![
+                self.halo.clone(),
+                self.m.get_type().src_type.clone()
+            ]).apply_substitution(&|k| self.σ.get(k).cloned())
+            .clone(),
+
+            dst_type: TypeTerm::Ladder(vec![
+                self.halo.clone(),
+                self.m.get_type().dst_type.clone()
+            ]).apply_substitution(&|k| self.σ.get(k).cloned())
+            .clone()
+        }.normalize()
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismPath<M: Morphism + Clone> {
+    pub weight: u64,
+    pub cur_type: TypeTerm,
+    pub morphisms: Vec< MorphismInstance<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct MorphismBase<M: Morphism + Clone> {
+    morphisms: Vec< M >,
+    seq_types: Vec< TypeTerm >
+}
+
+impl<M: Morphism + Clone> MorphismBase<M> {
+    pub fn new(seq_types: Vec<TypeTerm>) -> Self {
+        MorphismBase {
+            morphisms: Vec::new(),
+            seq_types
+        }
+    }
+
+    pub fn add_morphism(&mut self, m: M) {
+        self.morphisms.push( m );
+    }
+
+    pub fn enum_direct_morphisms(&self, src_type: &TypeTerm)
+    -> Vec< MorphismInstance<M> >
+    {
+        let mut dst_types = Vec::new();
+        for m in self.morphisms.iter() {
+            if let Ok((halo, σ)) = crate::unification::subtype_unify(
+                &src_type.clone().param_normalize(),
+                &m.get_type().src_type.param_normalize(),
+            ) {
+                dst_types.push(MorphismInstance{ halo, m: m.clone(), σ });
+            }
+        }
+        dst_types
+    }
+
+    pub fn enum_map_morphisms(&self, src_type: &TypeTerm)
+    -> Vec< MorphismInstance<M> > {
+        let src_type = src_type.clone().param_normalize();
+        let mut dst_types = Vec::new();
+
+        // Check if we have a List type, and if so, see what the Item type is
+        // TODO: function for generating fresh variables
+        let item_variable = TypeID::Var(800);
+
+        for seq_type in self.seq_types.iter() {
+            if let Ok((halo, σ)) = crate::unification::subtype_unify(
+                &src_type,
+                &TypeTerm::App(vec![
+                    seq_type.clone(),
+                    TypeTerm::TypeID(item_variable)
+                ])
+            ) {
+                let src_item_type = σ.get(&item_variable).expect("var not in unificator").clone();
+                for item_morph_inst in self.enum_morphisms( &src_item_type ) {
+
+                    let mut dst_halo_ladder = vec![ halo.clone() ];
+                    if item_morph_inst.halo != TypeTerm::unit() {
+                        dst_halo_ladder.push(
+                            TypeTerm::App(vec![
+                                seq_type.clone().get_lnf_vec().first().unwrap().clone(),
+                                item_morph_inst.halo.clone()
+                            ]));
+                    }
+
+                    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(),
+                                m: map_morph,
+                                σ: item_morph_inst.σ
+                            }
+                        );
+                    } else {
+                        eprintln!("could not get map morphism");
+                    }
+                }
+            }
+        }
+
+        dst_types
+    }
+
+    pub fn enum_morphisms(&self, src_type: &TypeTerm) -> Vec< MorphismInstance<M> > {
+        let mut dst_types = Vec::new();
+        dst_types.append(&mut self.enum_direct_morphisms(src_type));
+        dst_types.append(&mut self.enum_map_morphisms(src_type));
+        dst_types
+    }
+
+    /* try to find shortest morphism-path for a given type
+     */
+    pub fn find_morphism_path(&self, ty: MorphismType
+        /*, type_dict: &mut impl TypeDict*/
+    )
+    -> Option< Vec<MorphismInstance<M>> >
+    {
+        let ty = ty.normalize();
+        let mut queue = vec![
+            MorphismPath { weight: 0, cur_type: ty.src_type.clone(), morphisms: vec![] }
+        ];
+
+        while ! queue.is_empty() {
+            queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
+
+            if let Some(mut cur_path) = queue.pop() {
+                if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &ty.dst_type ) {
+                    // found path
+                    for n in cur_path.morphisms.iter_mut() {
+                        let mut new_σ = HashMap::new();
+                        for (k,v) in σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+                            );
+                        }
+                        for (k,v) in n.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| σ.get(k).cloned()).clone()
+                            );
+                        }
+
+                        n.σ = new_σ;
+                    }
+
+                    return Some(cur_path.morphisms);
+                }
+
+                //eprintln!("cur path (w ={}) : @ {}", cur_path.weight, cur_path.cur_type.clone().sugar(type_dict).pretty(type_dict, 0) );
+                for next_morph_inst in self.enum_morphisms(&cur_path.cur_type) {
+                    let dst_type = next_morph_inst.get_type().dst_type;
+
+                    let mut creates_loop = false;
+
+                    let mut new_path = cur_path.clone();
+                    for n in new_path.morphisms.iter_mut() {
+                        let mut new_σ = HashMap::new();
+                        for (k,v) in n.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
+                            );
+                        }
+                        for (k,v) in next_morph_inst.σ.iter() {
+                            new_σ.insert(
+                                k.clone(),
+                                v.clone().apply_substitution(&|k| next_morph_inst.σ.get(k).cloned()).clone()
+                            );
+                        }
+                        n.σ = new_σ;
+                    }
+
+                    for m in new_path.morphisms.iter() {
+                        if m.get_type().src_type == dst_type {
+                            creates_loop = true;
+                            //eprintln!("creates loop..");
+                            break;
+                        }
+                    }
+
+                    if ! creates_loop {
+                        /*eprintln!("next morph ? \n    {}\n--> {} ",
+                            next_morph_inst.get_type().src_type.sugar(type_dict).pretty(type_dict, 0),
+                            next_morph_inst.get_type().dst_type.sugar(type_dict).pretty(type_dict, 0)
+                        );
+                        eprintln!("....take!\n  :: halo = {}\n  :: σ = {:?}", next_morph_inst.halo.clone().sugar(type_dict).pretty(type_dict, 0), next_morph_inst.σ);
+                        */
+                        new_path.weight += next_morph_inst.m.weight();
+                        new_path.cur_type = dst_type;
+                        new_path.morphisms.push(next_morph_inst);
+                        queue.push(new_path);
+                    }
+                }
+            }
+        }
+        None
+    }
+
+    pub fn find_direct_morphism(&self,
+        ty: &MorphismType,
+        dict: &mut impl TypeDict
+    ) -> Option< MorphismInstance<M> > {
+        eprintln!("find direct morph");
+        for m in self.morphisms.iter() {
+            let ty = ty.clone().normalize();
+            let morph_type = m.get_type().normalize();
+
+            eprintln!("find direct morph:\n   {}  <=   {}",
+                            dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
+                        );
+
+            if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
+                eprintln!("halo: {}", dict.unparse(&halo));
+
+                let dst_type = TypeTerm::Ladder(vec![
+                    halo.clone(),
+                    morph_type.dst_type.clone()
+                ]);
+                eprintln!("----------->   {}  <=   {}",
+                    dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
+                );
+
+                /*
+                let unification_problem = UnificationProblem::new(
+                                vec![
+                                    ( ty.src_type, morph_type.src_type ),
+                                    ( morph_type.dst_type, ty.dst_type )
+                                ]
+                            );*/
+
+                if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
+                    eprintln!("match. halo2 = {}", dict.unparse(&halo2));
+                    return Some(MorphismInstance {
+                        m: m.clone(),
+                        halo: halo2,
+                        σ,
+                    });
+                }
+            }
+        }
+        None
+    }
+
+    pub fn find_map_morphism(&self, ty: &MorphismType, dict: &mut impl TypeDict) -> Option< MorphismInstance<M> > {
+        for seq_type in self.seq_types.iter() {
+            eprintln!("try seq type {:?}", seq_type);
+
+            eprintln!("");
+
+            if let Ok((halos, σ)) = UnificationProblem::new_sub(vec![
+                (ty.src_type.clone().param_normalize(),
+                    TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(100)) ])),
+                (TypeTerm::App(vec![ seq_type.clone(), TypeTerm::TypeID(TypeID::Var(101)) ]),
+                    ty.dst_type.clone().param_normalize()),
+            ]).solve() {
+                // TODO: use real fresh variable names
+                let item_morph_type = MorphismType {
+                    src_type: σ.get(&TypeID::Var(100)).unwrap().clone(),
+                    dst_type: σ.get(&TypeID::Var(101)).unwrap().clone(),
+                }.normalize();
+
+                //eprintln!("Map Morph: try to find item-morph with type {:?}", item_morph_type);
+                if let Some(item_morph_inst) = self.find_morphism( &item_morph_type, dict ) {
+                    if let Some( list_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) {
+                        return Some( MorphismInstance {
+                            m: list_morph,
+                            σ,
+                            halo: halos[0].clone()
+                        } );
+                    }
+                }
+            }
+        }
+
+        None
+    }
+
+    pub fn find_morphism(&self, ty: &MorphismType,
+        dict: &mut impl TypeDict
+    )
+    -> Option< MorphismInstance<M> > {
+        if let Some(m) = self.find_direct_morphism(ty, dict) {
+            return Some(m);
+        }
+        if let Some(m) = self.find_map_morphism(ty, dict) {
+            return Some(m);
+        }
+        None
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/test/mod.rs

@@ -7,4 +7,5 @@ pub mod pnf;
 pub mod subtype;
 pub mod substitution;
 pub mod unification;
+pub mod morphism;
 

src/test/morphism.rs

@@ -0,0 +1,218 @@
+use {
+    crate::{dict::*, morphism::*, parser::*, unparser::*, TypeTerm}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq)]
+struct DummyMorphism(MorphismType);
+
+impl Morphism for DummyMorphism {
+    fn get_type(&self) -> MorphismType {
+        self.0.clone().normalize()
+    }
+
+    fn map_morphism(&self, seq_type: TypeTerm) -> Option<DummyMorphism> {
+        Some(DummyMorphism(MorphismType {
+            src_type: TypeTerm::App(vec![
+                seq_type.clone(),
+                self.0.src_type.clone()
+            ]),
+
+            dst_type: TypeTerm::App(vec![
+                seq_type.clone(),
+                self.0.dst_type.clone()
+            ])
+        }))
+    }
+}
+
+fn morphism_test_setup() -> ( BimapTypeDict, MorphismBase<DummyMorphism> ) {
+    let mut dict = BimapTypeDict::new();
+    let mut base = MorphismBase::<DummyMorphism>::new( vec![ dict.parse("Seq").expect("") ] );
+
+    dict.add_varname("Radix".into());
+    dict.add_varname("SrcRadix".into());
+    dict.add_varname("DstRadix".into());
+
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<Digit Radix> ~ Char").unwrap(),
+            dst_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("<Digit Radix> ~ ℤ_2^64 ~ machine.UInt64").unwrap(),
+            dst_type: dict.parse("<Digit Radix> ~ Char").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
+            dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap(),
+            dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix>~ℤ_2^64~machine.UInt64>").unwrap()
+        })
+    );
+    base.add_morphism(
+        DummyMorphism(MorphismType{
+            src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix>~ℤ_2^64~machine.UInt64>").unwrap(),
+            dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix>~ℤ_2^64~machine.UInt64>").unwrap()
+        })
+    );
+
+    (dict, base)
+}
+
+#[test]
+fn test_morphism_path() {
+    let (mut dict, mut base) = morphism_test_setup();
+
+    let path = base.find_morphism_path(MorphismType {
+        src_type: dict.parse("ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(),
+        dst_type: dict.parse("ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap(),
+    });
+
+    fn print_subst(m: &std::collections::HashMap<TypeID, TypeTerm>, dict: &mut impl TypeDict) {
+        eprintln!("{{");
+
+        for (k,v) in m.iter() {
+            eprintln!("    {} --> {}",
+                dict.get_typename(k).unwrap(),
+                dict.unparse(v)
+            );
+        }
+
+        eprintln!("}}");
+    }
+
+    if let Some(path) = path.as_ref() {
+        for n in path.iter() {
+            eprintln!("
+ψ = {}
+morph {}
+  --> {}
+with
+            ",
+            n.halo.clone().sugar(&mut dict).pretty(&mut dict, 0),
+            n.m.get_type().src_type.sugar(&mut dict).pretty(&mut dict, 0),
+            n.m.get_type().dst_type.sugar(&mut dict).pretty(&mut dict, 0),
+            );
+            print_subst(&n.σ, &mut dict)
+        }
+    }
+
+    assert_eq!(
+        path,
+        Some(
+            vec![
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: dict.parse("ℕ ~ <PosInt 10 BigEndian>").unwrap(),
+                    m: DummyMorphism(MorphismType {
+                        src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(),
+                        dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"SrcRadix".into()).unwrap(), TypeTerm::Num(10)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16)),
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt SrcRadix LittleEndian> ~ <Seq <Digit SrcRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt DstRadix LittleEndian> ~ <Seq <Digit DstRadix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap()
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16)),
+                        (dict.get_typeid(&"DstRadix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: TypeTerm::unit(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("ℕ ~ <PosInt Radix LittleEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("ℕ ~ <PosInt Radix BigEndian> ~ <Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                    }),
+                },
+                MorphismInstance {
+                    σ: vec![
+                        (dict.get_typeid(&"Radix".into()).unwrap(), TypeTerm::Num(16))
+                    ].into_iter().collect(),
+                    halo: dict.parse("ℕ ~ <PosInt Radix BigEndian>").unwrap(),
+                    m: DummyMorphism(MorphismType{
+                        src_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap(),
+                        dst_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap()
+                    })
+                }
+            ]
+        )
+    );
+/*
+    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>>()
+        ))
+    );
+    */
+}

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((
@@ -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();

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