wip. rewrite path search & unification for Sugared Terms

deprecates the old term struct

src/dict.rs

@@ -25,11 +25,11 @@ pub trait TypeDict : Send + Sync {
         }
     }
 
-    fn get_typeid_creat(&mut self, tn: &String) -> TypeID {
-        if let Some(id) = self.get_typeid(tn) {
+    fn get_typeid_creat(&mut self, tn: &str) -> TypeID {
+        if let Some(id) = self.get_typeid(&tn.to_string()) {
             id
         } else {
-            self.add_typename(tn.clone())
+            self.add_typename(tn.to_string())
         }
     }
 }

src/lib.rs

@@ -1,21 +1,37 @@
+#![allow(mixed_script_confusables)]
 
 pub mod bimap;
 pub mod dict;
-pub mod term;
-pub mod substitution;
 
 pub mod lexer;
 pub mod parser;
 pub mod unparser;
-pub mod sugar;
 pub mod curry;
-pub mod lnf;
+
+pub mod lnf; // deprecated
+pub mod subtype; // deprecated
+
 pub mod pnf;
-pub mod subtype;
+pub mod pnf_sugared;
+
+pub mod term;
+pub mod sugar;
+
+pub mod substitution;
+pub mod substitution_sugared;
+
 pub mod unification;
+pub mod unification_sugared;
+
 pub mod morphism;
+pub mod morphism_sugared;
+
 pub mod morphism_base;
+pub mod morphism_base_sugared;
+
 pub mod morphism_path;
+pub mod morphism_path_sugared;
+
 pub mod steiner_tree;
 
 #[cfg(test)]

src/morphism.rs

@@ -1,6 +1,13 @@
 use {
     crate::{
-        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
+        pnf::splice_ladders,
+        substitution_sugared::SugaredSubstitution,
+        subtype_unify,
+        sugar::{SugaredStructMember, SugaredTypeTerm},
+        unification::UnificationProblem,
+        unification_sugared::SugaredUnificationProblem,
+        unparser::*,
+        TypeDict, TypeID, TypeTerm
     },
     std::{collections::HashMap, u64}
 };
@@ -11,11 +18,6 @@ use {
 pub struct MorphismType {
     pub src_type: TypeTerm,
     pub dst_type: TypeTerm,
-/*
-    pub subtype_bounds: Vec< (TypeTerm, TypeTerm) >,
-    pub trait_bounds: Vec< (TypeTerm, TypeTerm) >,
-    pub equal_bounds: Vec< (TypeTerm, TypeTerm) >,
-*/
 }
 
 impl MorphismType {
@@ -23,10 +25,6 @@ impl MorphismType {
         MorphismType {
             src_type: self.src_type.strip().param_normalize(),
             dst_type: self.dst_type.strip().param_normalize(),
-/*
-            subtype_bounds: Vec::new(),
-            trait_bounds: Vec::new()
-            */
         }
     }
 }
@@ -65,12 +63,6 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
                 self.m.get_type().dst_type.clone()
             ]).apply_subst(&self.σ)
             .clone(),
-/*
-            trait_bounds: Vec::new(),
-            subtype_bounds: Vec::new()
-            */
         }.normalize()
     }
 }
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_base.rs

@@ -1,9 +1,7 @@
 use {
     crate::{
-        subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm,
-        morphism::{MorphismType, Morphism, MorphismInstance}
-    },
-    std::{collections::HashMap, u64}
+        morphism::{Morphism, MorphismInstance, MorphismType}, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphismType}, subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, TypeDict, TypeID, TypeTerm
+    }
 };
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -101,29 +99,29 @@ impl<M: Morphism + Clone> MorphismBase<M> {
         ty: &MorphismType,
         dict: &mut impl TypeDict
     ) -> Option< MorphismInstance<M> > {
-        eprintln!("find direct morph");
+        //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));
+                //eprintln!("halo: {}", dict.unparse(&halo));
 
                 let dst_type = TypeTerm::Ladder(vec![
                     halo.clone(),
                     morph_type.dst_type.clone()
                 ]).normalize().param_normalize();
-
+/*
                 eprintln!("----------->   {}  <=   {}",
                     dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
                 );
-
+*/
                 if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
-                    eprintln!("match. halo2 = {}", dict.unparse(&halo2));
+                   //eprintln!("match. halo2 = {}", dict.unparse(&halo2));
                     return Some(MorphismInstance {
                         m: m.clone(),
                         halo,

src/morphism_base_sugared.rs

@@ -0,0 +1,143 @@
+use {
+    crate::{
+        morphism_path_sugared::{SugaredMorphismPath, SugaredShortestPathProblem}, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, sugar::SugaredTypeTerm, SugaredStructMember, TypeDict, TypeID, TypeTerm
+    }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SugaredMorphismBase<M: SugaredMorphism + Clone> {
+    morphisms: Vec< M >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
+    pub fn new() -> Self {
+        SugaredMorphismBase {
+            morphisms: Vec::new()
+        }
+    }
+
+    pub fn add_morphism(&mut self, m: M) {
+        self.morphisms.push( m );
+    }
+
+    pub fn get_morphism_instance(&self, ty: &SugaredMorphismType) -> Option<MorphismInstance2<M>> {
+        if let Some(path) = SugaredShortestPathProblem::new(self, ty.clone()).solve() {
+            if path.len() == 1 {
+                Some(path[0].clone())
+            } else {
+                Some(MorphismInstance2::Chain { path })
+            }
+        } else {
+            None
+        }
+    }
+
+    pub fn complex_morphism_decomposition(&self, src_type: &SugaredTypeTerm, dst_type: &SugaredTypeTerm) -> Option< MorphismInstance2<M> > {
+        let (src_ψ, src_floor) = src_type.get_floor_type();
+        let (dst_ψ, dst_floor) = dst_type.get_floor_type();
+
+        if !dst_ψ.is_empty() {
+            if !crate::unification_sugared::subtype_unify(&src_ψ, &dst_ψ).is_ok() {
+                return None;
+            }
+        }
+
+        match (src_floor, dst_floor) {
+            (SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs, members: members_lhs},
+                SugaredTypeTerm::Struct { struct_repr: _struct_repr_rhs, members: members_rhs })
+            => {
+                // todo: optimization: check if struct repr match
+
+                let mut member_morph = Vec::new();
+                let mut failed = false;
+                let mut necessary = false;
+
+                for SugaredStructMember{ symbol: symbol_rhs, ty: ty_rhs } in members_rhs.iter() {
+                    let mut found_src_member = false;
+                    for SugaredStructMember{ symbol: symbol_lhs, ty: ty_lhs } in members_lhs.iter() {
+                        if symbol_rhs == symbol_lhs {
+                            found_src_member = true;
+
+                            if let Some(mm) = self.get_morphism_instance(&SugaredMorphismType { src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+                                if ty_lhs != ty_rhs {
+                                    necessary = true;
+                                }
+                                member_morph.push((symbol_lhs.clone(), mm))
+                            } else {
+                                failed = true;
+                            }
+                            break;
+                        }
+                    }
+
+                    // member of rhs not found in lhs
+                    if ! found_src_member {
+                        failed = true;
+                        break;
+                    }
+                }
+
+                if ! failed && necessary {
+                    Some(MorphismInstance2::MapStruct {
+                        ψ: src_ψ,
+                        struct_repr: struct_repr_lhs.clone(),
+                        member_morph
+                    })
+                } else {
+                    None
+                }
+            }
+
+
+            (SugaredTypeTerm::Seq{ seq_repr: seq_repr_lhs, items: items_lhs },
+                SugaredTypeTerm::Seq{ seq_repr: _seq_rerpr_rhs, items: items_rhs })
+            => {
+                //let mut item_morphs = Vec::new();
+
+                for (ty_lhs, ty_rhs) in items_lhs.iter().zip(items_rhs.iter()) {
+                    if let Some(item_morph) = self.get_morphism_instance(&SugaredMorphismType{ src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+                        return Some(MorphismInstance2::MapSeq { ψ: src_ψ, seq_repr: seq_repr_lhs.clone(), item_morph: Box::new(item_morph) });
+                    }
+                    break;
+                }
+                None
+            }
+
+            _ => {
+                None
+            }
+        }
+    }
+
+    pub fn enum_morphisms_from(&self, src_type: &SugaredTypeTerm) -> Vec< MorphismInstance2<M> > {
+        let mut morphs = Vec::new();
+
+        for m in self.morphisms.iter() {
+            let m_src_type = m.get_type().src_type;
+            let m_dst_type = m.get_type().dst_type;
+
+            /* 1. primitive morphisms */
+
+            // check if the given start type is compatible with the
+            // morphisms source type,
+            // i.e. check if `src_type` is a subtype of `m_src_type`
+            if let Ok((ψ, σ)) = crate::unification_sugared::subtype_unify(src_type, &m_src_type) {
+                morphs.push(MorphismInstance2::Primitive { ψ, σ, morph: m.clone() });
+            }
+
+            /* 2. check complex types */
+            if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
+                morphs.push(complex_morph);
+            }
+        }
+
+        morphs
+    }
+
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_path.rs

@@ -39,10 +39,14 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
 
     pub fn solve(&mut self) -> Option< Vec<MorphismInstance<M>> > {
         while ! self.queue.is_empty() {
+            /* take the shortest partial path and try to advance it by one step */
             self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
 
             if let Some(mut cur_path) = self.queue.pop() {
-                if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
+
+                /* 1. Check if goal is already reached by the current path */
+
+                if let Ok((ψ, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
                     /* found path,
                      * now apply substitution and trim to variables in terms of each step
                      */
@@ -78,6 +82,9 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
                     return Some(cur_path.morphisms);
                 }
 
+                /* 2. Try to advance the path */
+                /* 2.1. Direct Morphisms */
+
                 //eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
                 for mut next_morph_inst in self.morphism_base.enum_morphisms(&cur_path.cur_type) {
                     let dst_type = next_morph_inst.get_type().dst_type;
@@ -125,6 +132,12 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
                         self.queue.push(new_path);
                     }
                 }
+
+                /* 2.2. Try to decompose */
+                /* 2.2.1.  Seq - Map */
+                /* 2.2.2.  Struct - Map */
+                /* 2.2.3.  Enum - Map */
+
             }
         }
         None

src/morphism_path_sugared.rs

@@ -0,0 +1,108 @@
+use {
+    crate::{
+        dict::*,
+        morphism_sugared::{SugaredMorphism, SugaredMorphismType, MorphismInstance2},
+        morphism_base_sugared::SugaredMorphismBase,
+        substitution_sugared::SugaredSubstitution,
+        sugar::*, term::*,
+    }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SugaredMorphismPath<M: SugaredMorphism + Clone> {
+    pub weight: u64,
+    pub cur_type: SugaredTypeTerm,
+    pub morphisms: Vec< MorphismInstance2<M> >
+}
+
+
+impl<M: SugaredMorphism+Clone> SugaredMorphismPath<M> {
+    fn apply_subst(&mut self, σ: &std::collections::HashMap<TypeID, SugaredTypeTerm>) {
+        for m in self.morphisms.iter_mut() {
+            m.apply_subst(σ);
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub struct SugaredShortestPathProblem<'a, M: SugaredMorphism + Clone> {
+    pub morphism_base: &'a SugaredMorphismBase<M>,
+    pub goal: SugaredTypeTerm,
+    queue: Vec< SugaredMorphismPath<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<'a, M:SugaredMorphism+Clone> SugaredShortestPathProblem<'a, M> {
+    pub fn new(morphism_base: &'a SugaredMorphismBase<M>, ty: SugaredMorphismType) -> Self {
+        SugaredShortestPathProblem {
+            morphism_base,
+            queue: vec![
+                SugaredMorphismPath::<M> { weight: 0, cur_type: ty.src_type, morphisms: vec![] }
+            ],
+            goal: ty.dst_type
+        }
+    }
+
+    pub fn advance(&mut self, prev_path: &SugaredMorphismPath<M>, morph_inst: MorphismInstance2<M>) {
+        let dst_type = morph_inst.get_type().dst_type;
+        //eprintln!("try morph to {:?}", dst_type.clone());//.sugar(type_dict).pretty(type_dict, 0));
+
+        let mut creates_loop = false;
+
+        let mut new_path = prev_path.clone();
+        for n in new_path.morphisms.iter_mut() {
+            n.apply_subst(&morph_inst.get_subst());
+        }
+
+        for m in new_path.morphisms.iter() {
+            if m.get_type().src_type == dst_type {
+                creates_loop = true;
+                break;
+            }
+        }
+
+        if ! creates_loop {
+            new_path.weight += 1;//next_morph_inst.get_weight();
+            new_path.cur_type = dst_type;
+
+            new_path.morphisms.push(morph_inst);
+            self.queue.push(new_path);
+        }
+    }
+
+    pub fn solve(&mut self) -> Option< Vec<MorphismInstance2<M>> > {
+        while ! self.queue.is_empty() {
+            /* take the shortest partial path and try to advance it by one step */
+            self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
+            if let Some(mut cur_path) = self.queue.pop() {
+
+                /* 1. Check if goal is already reached by the current path */
+                if let Ok((_ψ, σ)) = crate::unification_sugared::subtype_unify( &cur_path.cur_type, &self.goal ) {
+                    /* found path,
+                     * now apply substitution and trim to variables in terms of each step
+                     */
+                    cur_path.apply_subst(&σ);
+                    return Some(cur_path.morphisms);
+                }
+
+                /* 2. Try to advance current path */
+                else if let Some(complex_morph) =
+                    self.morphism_base.complex_morphism_decomposition( &cur_path.cur_type, &self.goal )
+                {
+                    self.advance(&cur_path, complex_morph);
+                } else {
+                    for next_morph_inst in self.morphism_base.enum_morphisms_from(&cur_path.cur_type) {
+                        self.advance(&cur_path, next_morph_inst);
+                    }
+                }
+            }
+        }
+        None
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/morphism_sugared.rs

@@ -0,0 +1,205 @@
+use {
+    crate::{
+        substitution_sugared::SugaredSubstitution,
+        sugar::{SugaredStructMember, SugaredTypeTerm},
+        unification::UnificationProblem,
+        unification_sugared::SugaredUnificationProblem,
+        unparser::*, TypeDict,
+        TypeID, TypeTerm
+    },
+    std::{collections::HashMap, u64}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SugaredMorphismType {
+    pub src_type: SugaredTypeTerm,
+    pub dst_type: SugaredTypeTerm
+}
+
+pub trait SugaredMorphism : Sized {
+    fn get_type(&self) -> SugaredMorphismType;
+    fn weight(&self) -> u64 {
+        1
+    }
+}
+
+#[derive(Clone)]
+pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
+    Primitive{
+        ψ: SugaredTypeTerm,
+        σ: HashMap<TypeID, SugaredTypeTerm>,
+        morph: M,
+    },
+    Chain{
+        path: Vec<MorphismInstance2<M>>
+    },
+    MapSeq{
+        ψ: SugaredTypeTerm,
+        seq_repr: Option<Box<SugaredTypeTerm>>,
+        item_morph: Box<MorphismInstance2<M>>,
+    },
+    MapStruct{
+        ψ: SugaredTypeTerm,
+        struct_repr: Option<Box<SugaredTypeTerm>>,
+        member_morph: Vec< (String, MorphismInstance2<M>) >
+    },
+    MapEnum{
+        ψ: SugaredTypeTerm,
+        enum_repr: Option<Box<SugaredTypeTerm>>,
+        variant_morph: Vec< (String, MorphismInstance2<M>) >
+    }
+}
+
+
+impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
+    pub fn get_type(&self) -> SugaredMorphismType {
+        match self {
+            MorphismInstance2::Primitive { ψ, σ, morph } => {
+                SugaredMorphismType {
+                    src_type:
+                        SugaredTypeTerm::Ladder(vec![
+                            ψ.clone(),
+                            morph.get_type().src_type
+                                .apply_subst(σ).clone()
+                        ]).strip(),
+
+                    dst_type: SugaredTypeTerm::Ladder(vec![
+                            ψ.clone(),
+                            morph.get_type().dst_type
+                                .apply_subst(σ).clone()
+                        ]).strip(),
+                }
+            }
+            MorphismInstance2::Chain { path } => {
+                if path.len() > 0 {
+                    SugaredMorphismType {
+                        src_type: path.first().unwrap().get_type().src_type,
+                        dst_type: path.last().unwrap().get_type().dst_type
+                    }
+                } else {
+                    SugaredMorphismType {
+                        src_type: SugaredTypeTerm::TypeID(TypeID::Var(45454)),
+                        dst_type: SugaredTypeTerm::TypeID(TypeID::Var(45454))
+                    }
+                }
+            }
+            MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+                SugaredMorphismType {
+                    src_type: SugaredTypeTerm::Ladder(vec![
+                        ψ.clone(),
+                        SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
+                            items: vec![ item_morph.get_type().src_type ]}
+                    ]).strip(),
+                    dst_type: SugaredTypeTerm::Ladder(vec![
+                        ψ.clone(),
+                        SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
+                            items: vec![ item_morph.get_type().dst_type ]}
+                    ]).strip()
+                }
+            }
+            MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+                SugaredMorphismType {
+                    src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+                            SugaredTypeTerm::Struct{
+                                struct_repr: struct_repr.clone(),
+                                members:
+                                    member_morph.iter().map(|(symbol, morph)| {
+                                       SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+                                    }).collect()
+                            }
+                        ]).strip(),
+                    dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+                            SugaredTypeTerm::Struct{
+                                struct_repr: struct_repr.clone(),
+                                members: member_morph.iter().map(|(symbol, morph)| {
+                                    SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+                                }).collect()
+                            }
+                        ]).strip()
+                }
+            }
+            MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+                SugaredMorphismType {
+                    src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+                            SugaredTypeTerm::Struct{
+                                struct_repr: enum_repr.clone(),
+                                members:
+                                    variant_morph.iter().map(|(symbol, morph)| {
+                                       SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+                                    }).collect()
+                            }
+                        ]).strip(),
+                    dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+                            SugaredTypeTerm::Struct{
+                                struct_repr: enum_repr.clone(),
+                                members: variant_morph.iter().map(|(symbol, morph)| {
+                                    SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+                                }).collect()
+                            }
+                        ]).strip()
+                }
+            }
+        }
+    }
+
+    pub fn get_subst(&self) -> std::collections::HashMap< TypeID, SugaredTypeTerm > {
+        match self {
+            MorphismInstance2::Primitive { ψ, σ, morph } => σ.clone(),
+            MorphismInstance2::Chain { path } => {
+                path.iter().fold(
+                    std::collections::HashMap::new(),
+                    |mut σ, m| {
+                        σ = σ.append(&m.get_subst());
+                        σ
+                    }
+                )
+            },
+            MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+                item_morph.get_subst()
+            },
+            MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+                let mut σ = HashMap::new();
+                for (symbol, m) in member_morph.iter() {
+                    σ = σ.append(&mut m.get_subst());
+                }
+                σ
+            },
+            MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+                todo!();
+                HashMap::new()
+            },
+        }
+    }
+
+    pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, SugaredTypeTerm >) {
+        match self {
+            MorphismInstance2::Primitive { ψ, σ, morph } => {
+                ψ.apply_subst(σ);
+                *σ = σ.clone().append(γ);
+            },
+            MorphismInstance2::Chain { path } => {
+                for n in path.iter_mut() {
+                    n.apply_subst(γ);
+                }
+            }
+            MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+                ψ.apply_subst(γ);
+                item_morph.apply_subst(γ);
+            }
+            MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+                for (_,ty) in member_morph {
+                    ty.apply_subst(γ);
+                }
+            },
+            MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+                for (_,ty) in variant_morph {
+                    ty.apply_subst(γ);
+                }
+            }
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/pnf_sugared.rs

@@ -0,0 +1,161 @@
+use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm >  ) -> Vec< SugaredTypeTerm > {
+    for i in 0 .. upper.len() {
+        if upper[i] == lower[0] {
+            let mut result_ladder = Vec::<SugaredTypeTerm>::new();
+            result_ladder.append(&mut upper[0..i].iter().cloned().collect());
+            result_ladder.append(&mut lower);
+            return result_ladder;
+        }
+    }
+
+    upper.append(&mut lower);
+    upper
+}
+
+impl SugaredTypeTerm {
+    /// transmute type into Parameter-Normal-Form (PNF)
+    ///
+    /// Example:
+    /// ```ignore
+    /// <Seq <Digit 10>>~<Seq Char>
+    /// ⇒ <Seq <Digit 10>~Char>
+    /// ```
+    pub fn param_normalize(mut self) -> Self {
+
+        match self {
+            SugaredTypeTerm::Ladder(mut rungs) => {
+                if rungs.len() > 0 {
+                    let mut new_rungs = Vec::new();
+                    while let Some(bottom) = rungs.pop() {
+                        if let Some(last_but) = rungs.last_mut() {
+                            match (bottom, last_but) {
+                                (SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
+                                    if bot_args.len() == last_args.len() {
+                                        let mut new_rung_params = Vec::new();
+                                        let mut require_break = false;
+
+                                        if bot_args.len() > 0 {
+                                            todo!();
+                                            /*
+                                            if let Ok(_idx) =  last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
+                                                for i in 0 .. bot_args.len() {
+
+                                                    let spliced_type_ladder = splice_ladders(
+                                                        last_args[i].clone().get_lnf_vec(),
+                                                        bot_args[i].clone().get_lnf_vec()
+                                                    );
+                                                    let spliced_type =
+                                                        if spliced_type_ladder.len() == 1 {
+                                                            spliced_type_ladder[0].clone()
+                                                        } else if spliced_type_ladder.len() > 1 {
+                                                            SugaredTypeTerm::Ladder(spliced_type_ladder)
+                                                        } else {
+                                                            SugaredTypeTerm::unit()
+                                                        };
+
+                                                    new_rung_params.push( spliced_type.param_normalize() );
+                                                }
+
+                                            } else {
+                                                new_rung_params.push(
+                                                    SugaredTypeTerm::Ladder(vec![
+                                                        last_args[0].clone(),
+                                                        bot_args[0].clone()
+                                                    ])//.normalize()
+                                                );
+
+                                                for i in 1 .. bot_args.len() {
+                                                    if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
+                                                        let spliced_type_ladder = splice_ladders(
+                                                            last_args[i].clone().get_lnf_vec(),
+                                                            bot_args[i].clone().get_lnf_vec()
+                                                        );
+                                                        let spliced_type =
+                                                            if spliced_type_ladder.len() == 1 {
+                                                                spliced_type_ladder[0].clone()
+                                                            } else if spliced_type_ladder.len() > 1 {
+                                                                SugaredTypeTerm::Ladder(spliced_type_ladder)
+                                                            } else {
+                                                                SugaredTypeTerm::unit()
+                                                            };
+
+                                                        new_rung_params.push( spliced_type.param_normalize() );
+                                                    } else {
+                                                        new_rung_params.push( bot_args[i].clone() );
+                                                        require_break = true;
+                                                    }
+                                                }
+                                            }
+                                            */
+                                        }
+
+                                        if require_break {
+                                            new_rungs.push( SugaredTypeTerm::Spec(new_rung_params) );
+                                        } else {
+                                            rungs.pop();
+                                            rungs.push(SugaredTypeTerm::Spec(new_rung_params));
+                                        }
+
+                                    } else {
+                                        new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
+                                    }
+                                }
+                                (bottom, last_buf) => {
+                                    new_rungs.push( bottom );
+                                }
+                            }
+                        } else {
+                            new_rungs.push( bottom );
+                        }
+                    }
+
+                    new_rungs.reverse();
+
+                    if new_rungs.len() > 1 {
+                        SugaredTypeTerm::Ladder(new_rungs)
+                    } else if new_rungs.len() == 1 {
+                        new_rungs[0].clone()
+                    } else {
+                        SugaredTypeTerm::unit()
+                    }
+                } else {
+                    SugaredTypeTerm::unit()
+                }
+            }
+
+            SugaredTypeTerm::Spec(params) => {
+                SugaredTypeTerm::Spec(
+                    params.into_iter()
+                        .map(|p| p.param_normalize())
+                        .collect())
+            }
+
+            SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
+                seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
+                items: items.into_iter().map(|p| p.param_normalize()).collect()
+            },
+            SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
+                struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
+                members: members.into_iter()
+                    .map(|SugaredStructMember{symbol, ty}|
+                        SugaredStructMember{ symbol, ty: ty.param_normalize() })
+                    .collect()
+            },
+            SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
+                enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
+                variants: variants.into_iter()
+                    .map(|SugaredEnumVariant{symbol, ty}|
+                        SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
+                    .collect()
+            },
+
+            atomic => atomic
+        }
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/pretty.rs

@@ -5,18 +5,18 @@ use {
 
 
 impl SugaredStructMember {
-    pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
         format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
     }
 }
 impl SugaredEnumVariant {
-    pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
         format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
     }
 }
 
 impl SugaredTypeTerm {
-    pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+    pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
         let indent_width = 4;
         match self {
             SugaredTypeTerm::TypeID(id) => {
@@ -64,15 +64,20 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Struct(args) => {
+            SugaredTypeTerm::Struct{ struct_repr, members } => {
                 let mut s = String::new();
                 s.push_str(&"{".yellow().bold());
-                for arg in args {
+
+                if let Some(struct_repr) = struct_repr {
+                    s.push_str(&format!("{}{} ", "~".yellow(), struct_repr.pretty(dict, indent+1)));
+                }
+
+                for member in members {
                     s.push('\n');
                     for x in 0..(indent+1)*indent_width {
                         s.push(' ');
                     }
-                    s.push_str(&arg.pretty(dict, indent + 1));
+                    s.push_str(&member.pretty(dict, indent + 1));
                     s.push_str(&";\n".bright_yellow());
                 }
 
@@ -84,11 +89,16 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Enum(args) => {
+            SugaredTypeTerm::Enum{ enum_repr, variants } => {
                 let mut s = String::new();
                 s.push_str(&"(".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
+
+                if let Some(enum_repr) = enum_repr {
+                    s.push_str(&format!("{}{} ", "~".yellow(), enum_repr.pretty(dict, indent+1)));
+                }
+
+
+                for (i,variant) in variants.iter().enumerate() {
                     s.push('\n');
                     for x in 0..(indent+1)*indent_width {
                         s.push(' ');
@@ -96,7 +106,7 @@ impl SugaredTypeTerm {
                     if i > 0 {
                         s.push_str(&"| ".yellow().bold());
                     }
-                    s.push_str(&arg.pretty(dict, indent + 1));
+                    s.push_str(&variant.pretty(dict, indent + 1));
                 }
 
                 s.push('\n');
@@ -107,15 +117,20 @@ impl SugaredTypeTerm {
                 s
             }
 
-            SugaredTypeTerm::Seq(args) => {
+            SugaredTypeTerm::Seq{ seq_repr, items } => {
                 let mut s = String::new();
-                s.push_str(&"[ ".yellow().bold());
-                for i in 0..args.len() {
-                    let arg = &args[i];
+                s.push_str(&"[".yellow().bold());
+
+                if let Some(seq_repr) = seq_repr {
+                    s.push_str(&format!("{}{}", "~".yellow(), seq_repr.pretty(dict, indent+1)));
+                }
+                s.push(' ');
+
+                for (i, item) in items.iter().enumerate() {
                     if i > 0 {
                         s.push(' ');
                     }
-                    s.push_str(&arg.pretty(dict, indent+1));
+                    s.push_str(&item.pretty(dict, indent+1));
                 }
                 s.push_str(&" ]".yellow().bold());
                 s

src/substitution.rs

@@ -60,3 +60,5 @@ impl TypeTerm {
         self
     }
 }
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/substitution_sugared.rs

@@ -0,0 +1,114 @@
+
+use std::ops::DerefMut;
+use crate::{
+    TypeID,
+    TypeTerm
+};
+use crate::sugar::*;
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub trait SugaredSubstitution {
+    fn get(&self, t: &TypeID) -> Option< SugaredTypeTerm >;
+    fn add(&mut self, tyid: TypeID, val: SugaredTypeTerm);
+    fn append(self, rhs: &Self) -> Self;
+}
+
+impl SugaredSubstitution for std::collections::HashMap< TypeID, SugaredTypeTerm > {
+    fn get(&self, t: &TypeID) -> Option< SugaredTypeTerm > {
+        (self as &std::collections::HashMap< TypeID, SugaredTypeTerm >).get(t).cloned()
+    }
+
+    fn add(&mut self, tyid: TypeID, val: SugaredTypeTerm) {
+        if let TypeID::Var(id) = tyid {
+            if !val.contains_var(id) {
+                self.insert(tyid, val);
+            } else {
+                eprintln!("substitution cannot contain loop");
+            }
+        }
+    }
+
+    fn append(self, rhs: &Self) -> Self {
+        let mut new_σ = std::collections::HashMap::new();
+        for (v, tt) in self.iter() {
+            let mut tt = tt.clone();
+            tt.apply_subst(rhs);
+            tt.apply_subst(&self);
+            new_σ.add(v.clone(), tt);
+        }
+        for (v, tt) in rhs.iter() {
+            new_σ.add(v.clone(), tt.clone());
+        }
+
+        new_σ
+    }
+}
+
+impl SugaredTypeTerm {
+    /// recursively apply substitution to all subterms,
+    /// which will replace all occurences of variables which map
+    /// some type-term in `subst`
+    pub fn apply_substitution(
+        &mut self,
+        σ: &impl SugaredSubstitution
+    ) -> &mut Self {
+        self.apply_subst(σ)
+    }
+
+    pub fn apply_subst(
+        &mut self,
+        σ: &impl SugaredSubstitution
+    ) -> &mut Self {
+        match self {
+            SugaredTypeTerm::Num(_) => {},
+            SugaredTypeTerm::Char(_) => {},
+
+            SugaredTypeTerm::TypeID(typid) => {
+                if let Some(t) = σ.get(typid) {
+                    *self = t;
+                }
+            }
+            SugaredTypeTerm::Ladder(args) |
+            SugaredTypeTerm::Spec(args) |
+            SugaredTypeTerm::Func(args) |
+            SugaredTypeTerm::Morph(args)
+            => {
+                for r in args.iter_mut() {
+                    r.apply_subst(σ);
+                }
+            }
+
+            SugaredTypeTerm::Univ(t) => { t.apply_subst(σ); }
+
+            SugaredTypeTerm::Struct { struct_repr, members } => {
+                if let Some(struct_repr) = struct_repr.as_mut() {
+                    struct_repr.apply_subst(σ);
+                }
+                for SugaredStructMember{ symbol:_, ty } in members.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            },
+            SugaredTypeTerm::Enum { enum_repr, variants } => {
+                if let Some(enum_repr) = enum_repr.as_mut() {
+                    enum_repr.apply_subst(σ);
+                }
+                for SugaredEnumVariant{ symbol:_, ty } in variants.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            }
+            SugaredTypeTerm::Seq { seq_repr, items } => {
+                if let Some(seq_repr) = seq_repr {
+                    seq_repr.apply_subst(σ);
+                }
+                for ty in items.iter_mut() {
+                    ty.apply_subst(σ);
+                }
+            },
+        }
+
+        self
+    }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/subtype.rs

@@ -2,7 +2,7 @@ use crate::term::TypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
-impl TypeTerm {    
+impl TypeTerm {
     // returns ladder-step of first match and provided representation-type
     pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
         let provided_lnf = self.clone().get_lnf_vec();
@@ -49,3 +49,28 @@ impl TypeTerm {
 }
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+use crate::sugar::*;
+
+impl SugaredTypeTerm {
+    pub fn is_compatible(&self, supertype: SugaredTypeTerm) -> bool {
+        match (self, supertype) {
+            (SugaredTypeTerm::TypeID(idl), SugaredTypeTerm::TypeID(idr)) => {
+                if *idl == idr {
+                    true
+                } else {
+                    false
+                }
+            }
+
+
+            (SugaredTypeTerm::Ladder(l_rungs), SugaredTypeTerm::Ladder(r_rungs)) => {
+                false
+            }
+
+            _ => {
+                false
+            }
+        }
+    }
+}

src/sugar.rs

@@ -1,20 +1,20 @@
 use {
-    crate::{parser::ParseLadderType, TypeDict, TypeID, TypeTerm}
+    crate::{parser::ParseLadderType, subtype_unify, TypeDict, TypeID, TypeTerm}
 };
 
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct SugaredStructMember {
     pub symbol: String,
     pub ty: SugaredTypeTerm
 }
 
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub struct SugaredEnumVariant {
     pub symbol: String,
     pub ty: SugaredTypeTerm
 }
 
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
 pub enum SugaredTypeTerm {
     TypeID(TypeID),
     Num(i64),
@@ -24,24 +24,37 @@ pub enum SugaredTypeTerm {
     Func(Vec< SugaredTypeTerm >),
     Morph(Vec< SugaredTypeTerm >),
     Ladder(Vec< SugaredTypeTerm >),
-    Struct(Vec< SugaredStructMember >),
-    Enum(Vec< SugaredEnumVariant >),
-    Seq(Vec< SugaredTypeTerm >)
+    Struct{
+        struct_repr: Option< Box<SugaredTypeTerm> >,
+        members: Vec< SugaredStructMember >
+    },
+    Enum{
+        enum_repr: Option<Box< SugaredTypeTerm >>,
+        variants: Vec< SugaredEnumVariant >
+    },
+    Seq{
+        seq_repr: Option<Box< SugaredTypeTerm >>,
+        items: Vec< SugaredTypeTerm >
+    },
+
+    /*
+    Todo: Ref, RefMut
+    */
 }
 
 impl SugaredStructMember {
     pub fn parse( dict: &mut impl TypeDict, ty: &TypeTerm ) -> Option<Self> {
         match ty {
             TypeTerm::App(args) => {
-                if args.len() != 3 {
+                if args.len() != 2 {
                     return None;
                 }
-
+/*
                 if args[0] != dict.parse("Struct.Field").expect("parse") {
                     return None;
                 }
-
-                let symbol = match args[1] {
+*/
+                let symbol = match args[0] {
                     TypeTerm::Char(c) => c.to_string(),
                     TypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
                     _ => {
@@ -49,7 +62,7 @@ impl SugaredStructMember {
                     }
                 };
 
-                let ty = args[2].clone().sugar(dict);
+                let ty = args[1].clone().sugar(dict);
 
                 Some(SugaredStructMember { symbol, ty })
             }
@@ -64,15 +77,15 @@ impl SugaredEnumVariant {
     pub fn parse( dict: &mut impl TypeDict, ty: &TypeTerm ) -> Option<Self> {
         match ty {
             TypeTerm::App(args) => {
-                if args.len() != 3 {
+                if args.len() != 2 {
                     return None;
                 }
-
+/*
                 if args[0] != dict.parse("Enum.Variant").expect("parse") {
                     return None;
                 }
-
-                let symbol = match args[1] {
+*/
+                let symbol = match args[0] {
                     TypeTerm::Char(c) => c.to_string(),
                     TypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
                     _ => {
@@ -80,7 +93,7 @@ impl SugaredEnumVariant {
                     }
                 };
 
-                let ty = args[2].clone().sugar(dict);
+                let ty = args[1].clone().sugar(dict);
 
                 Some(SugaredEnumVariant { symbol, ty })
             }
@@ -93,6 +106,10 @@ impl SugaredEnumVariant {
 
 impl TypeTerm {
     pub fn sugar(self: TypeTerm, dict: &mut impl crate::TypeDict) -> SugaredTypeTerm {
+        dict.add_varname("StructRepr".into());
+        dict.add_varname("EnumRepr".into());
+        dict.add_varname("SeqRepr".into());
+
         match self {
             TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
             TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
@@ -105,13 +122,52 @@ impl TypeTerm {
                     SugaredTypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
                 }
                 else if first == &dict.parse("Struct").unwrap() {
-                    SugaredTypeTerm::Struct( args[1..].into_iter().map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field")).collect() )
+                    SugaredTypeTerm::Struct{
+                        struct_repr: None,
+                        members: args[1..].into_iter()
+                            .map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field"))
+                            .collect()
+                    }
+                }
+                else if let Ok(σ) = crate::unify( first, &dict.parse("Struct ~ StructRepr").expect("") ) {
+                    SugaredTypeTerm::Struct{
+                        struct_repr: Some(Box::new(σ.get(&dict.get_typeid(&"StructRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+                        members: args[1..].into_iter()
+                            .map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field"))
+                            .collect()
+                    }
                 }
                 else if first == &dict.parse("Enum").unwrap() {
-                    SugaredTypeTerm::Enum( args[1..].into_iter().map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant")).collect() )
+                    SugaredTypeTerm::Enum{
+                        enum_repr: None,
+                        variants: args[1..].into_iter()
+                            .map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant"))
+                            .collect()
+                    }
+                }
+                else if let Ok(σ) = crate::unify( first, &dict.parse("Enum ~ EnumRepr").expect("") ) {
+                    SugaredTypeTerm::Enum{
+                        enum_repr: Some(Box::new(σ.get(&dict.get_typeid(&"EnumRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+                        variants: args[1..].into_iter()
+                            .map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant"))
+                            .collect()
+                    }
                 }
                 else if first == &dict.parse("Seq").unwrap() {
-                    SugaredTypeTerm::Seq( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
+                    SugaredTypeTerm::Seq {
+                        seq_repr: None,
+                        items: args[1..].into_iter()
+                            .map(|t| t.clone().sugar(dict))
+                            .collect()
+                    }
+                }
+                else if let Ok(σ) = crate::unify( first, &dict.parse("Seq ~ SeqRepr").expect("") ) {
+                    SugaredTypeTerm::Seq {
+                        seq_repr: Some(Box::new(σ.get(&dict.get_typeid(&"SeqRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+                        items: args[1..].into_iter()
+                            .map(|t| t.clone().sugar(dict))
+                            .collect()
+                    }
                 }
                 else if first == &dict.parse("Spec").unwrap() {
                     SugaredTypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
@@ -139,7 +195,7 @@ impl TypeTerm {
 impl SugaredStructMember {
     pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
         TypeTerm::App(vec![
-            dict.parse("Struct.Field").expect("parse"),
+            //dict.parse("Struct.Field").expect("parse"),
             dict.parse(&self.symbol).expect("parse"),
             self.ty.desugar(dict)
         ])
@@ -149,7 +205,7 @@ impl SugaredStructMember {
 impl SugaredEnumVariant {
     pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
         TypeTerm::App(vec![
-            dict.parse("Enum.Variant").expect("parse"),
+            //dict.parse("Enum.Variant").expect("parse"),
             dict.parse(&self.symbol).expect("parse"),
             self.ty.desugar(dict)
         ])
@@ -157,6 +213,10 @@ impl SugaredEnumVariant {
 }
 
 impl SugaredTypeTerm {
+    pub fn unit() -> Self {
+        SugaredTypeTerm::Ladder(vec![])
+    }
+
     pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
         match self {
             SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
@@ -173,21 +233,270 @@ impl SugaredTypeTerm {
                 std::iter::once( dict.parse("Morph").unwrap() ).chain(
                     ts.into_iter().map(|t| t.desugar(dict))
                 ).collect()),
-            SugaredTypeTerm::Struct(ts) => TypeTerm::App(
-                std::iter::once( dict.parse("Struct").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
+            SugaredTypeTerm::Struct{ struct_repr, members } => TypeTerm::App(
+                std::iter::once(
+                    if let Some(sr) = struct_repr {
+                        TypeTerm::Ladder(vec![
+                            dict.parse("Struct").unwrap(),
+                            sr.desugar(dict)
+                        ])
+                    } else {
+                        dict.parse("Struct").unwrap()
+                    }
+                ).chain(
+                    members.into_iter().map(|t| t.desugar(dict))
                 ).collect()),
-            SugaredTypeTerm::Enum(ts) => TypeTerm::App(
+            SugaredTypeTerm::Enum{ enum_repr, variants } => TypeTerm::App(
                 std::iter::once( dict.parse("Enum").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
+                    variants.into_iter().map(|t| t.desugar(dict))
                 ).collect()),
-            SugaredTypeTerm::Seq(ts) => TypeTerm::App(
+            SugaredTypeTerm::Seq{ seq_repr, items } => TypeTerm::App(
                 std::iter::once( dict.parse("Seq").unwrap() ).chain(
-                    ts.into_iter().map(|t| t.desugar(dict))
+                    items.into_iter().map(|t| t.desugar(dict))
                 ).collect()),
         }
     }
 
+    pub fn contains_var(&self, var_id: u64) -> bool {
+        match self {
+            SugaredTypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+            SugaredTypeTerm::Spec(args) |
+            SugaredTypeTerm::Func(args) |
+            SugaredTypeTerm::Morph(args) |
+            SugaredTypeTerm::Ladder(args) => {
+                for a in args.iter() {
+                    if a.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            SugaredTypeTerm::Univ(t) => {
+                t.contains_var(var_id)
+            }
+            SugaredTypeTerm::Struct { struct_repr, members } => {
+                if let Some(struct_repr) =  struct_repr {
+                    if struct_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for SugaredStructMember{ symbol, ty } in members {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            SugaredTypeTerm::Enum { enum_repr, variants } => {
+                if let Some(enum_repr) =  enum_repr {
+                    if enum_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for SugaredEnumVariant{ symbol, ty } in variants {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+            SugaredTypeTerm::Seq { seq_repr, items } => {
+                if let Some(seq_repr) =  seq_repr {
+                    if seq_repr.contains_var(var_id) {
+                        return true;
+                    }
+                }
+
+                for ty in items {
+                    if ty.contains_var(var_id) {
+                        return true;
+                    }
+                }
+                false
+            }
+
+            SugaredTypeTerm::Num(_) |
+            SugaredTypeTerm::Char(_) |
+            SugaredTypeTerm::TypeID(TypeID::Fun(_)) => false
+        }
+    }
+
+    pub fn strip(self) -> SugaredTypeTerm {
+        if self.is_empty() {
+            return SugaredTypeTerm::unit();
+        }
+
+        match self {
+            SugaredTypeTerm::Ladder(rungs) => {
+                let mut rungs :Vec<_> = rungs.into_iter()
+                    .filter_map(|mut r| {
+                        r = r.strip();
+                        if r != SugaredTypeTerm::unit() {
+                            Some(match r {
+                                SugaredTypeTerm::Ladder(r) => r,
+                                a => vec![ a ]
+                            })
+                        }
+                        else { None }
+                    })
+                .flatten()
+                .collect();
+
+                if rungs.len() == 1 {
+                    rungs.pop().unwrap()
+                } else {
+                    SugaredTypeTerm::Ladder(rungs)
+                }
+            },
+            SugaredTypeTerm::Spec(args) => {
+                let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
+                if args.len() == 0 {
+                    SugaredTypeTerm::unit()
+                } else if args.len() == 1 {
+                    args.pop().unwrap()
+                } else {
+                    SugaredTypeTerm::Spec(args)
+                }
+            }
+            SugaredTypeTerm::Seq{ mut seq_repr, mut items } => {
+                if let Some(seq_repr) = seq_repr.as_mut() {
+                    *seq_repr = Box::new(seq_repr.clone().strip());
+                }
+                for i in items.iter_mut() {
+                    *i = i.clone().strip();
+                }
+
+                SugaredTypeTerm::Seq { seq_repr, items }
+            }
+            atom => atom
+        }
+    }
+
+
+    pub fn get_interface_type(&self) -> SugaredTypeTerm {
+        match self {
+            SugaredTypeTerm::Ladder(rungs) => {
+                if let Some(top) = rungs.first() {
+                    top.get_interface_type()
+                } else {
+                    SugaredTypeTerm::unit()
+                }
+            }
+            SugaredTypeTerm::Spec(args)
+                => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
+
+            SugaredTypeTerm::Func(args)
+                => SugaredTypeTerm::Func(args.iter().map(|a| a.get_interface_type()).collect()),
+
+            SugaredTypeTerm::Morph(args)
+                => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
+
+            SugaredTypeTerm::Univ(t)
+                => SugaredTypeTerm::Univ(Box::new(t.get_interface_type())),
+
+            SugaredTypeTerm::Seq { seq_repr, items } => {
+                SugaredTypeTerm::Seq {
+                    seq_repr: if let Some(sr) = seq_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    items: items.iter().map(|t| t.get_interface_type()).collect()
+                }
+            }
+            SugaredTypeTerm::Struct { struct_repr, members } => {
+                SugaredTypeTerm::Struct {
+                    struct_repr: if let Some(sr) = struct_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    members: members.iter()
+                        .map(|SugaredStructMember{symbol,ty}|
+                            SugaredStructMember {symbol:symbol.clone(), ty:ty.get_interface_type() })
+                        .collect()
+                }
+            }
+            SugaredTypeTerm::Enum { enum_repr, variants } => {
+                SugaredTypeTerm::Enum {
+                    enum_repr: if let Some(sr) = enum_repr {
+                        Some(Box::new(sr.clone().get_interface_type()))
+                    } else { None },
+                    variants: variants.iter()
+                        .map(|SugaredEnumVariant{symbol,ty}|
+                            SugaredEnumVariant{ symbol:symbol.clone(), ty:ty.get_interface_type() })
+                        .collect()
+                }
+            }
+
+            SugaredTypeTerm::TypeID(tyid) => SugaredTypeTerm::TypeID(tyid.clone()),
+            SugaredTypeTerm::Num(n) => SugaredTypeTerm::Num(*n),
+            SugaredTypeTerm::Char(c) => SugaredTypeTerm::Char(*c)
+        }
+    }
+
+    pub fn get_floor_type(&self) -> (SugaredTypeTerm, SugaredTypeTerm) {
+        match self.clone() {
+            SugaredTypeTerm::Ladder(mut rungs) => {
+                if let Some(bot) = rungs.pop() {
+                    let (bot_ψ, bot_floor) = bot.get_floor_type();
+                    rungs.push(bot_ψ);
+                    (SugaredTypeTerm::Ladder(rungs).strip(), bot_floor.strip())
+                } else {
+                    (SugaredTypeTerm::unit(), SugaredTypeTerm::unit())
+                }
+            }
+            /*
+            SugaredTypeTerm::Spec(args)
+                => (SugaredTypeTerm::SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Func(args)
+                => SugaredTypeTerm::Func(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Morph(args)
+                => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+            SugaredTypeTerm::Univ(t)
+                => SugaredTypeTerm::Univ(Box::new(t.get_floor_type())),
+
+            SugaredTypeTerm::Seq { seq_repr, items } => {
+                SugaredTypeTerm::Seq {
+                    seq_repr: if let Some(sr) = seq_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    items: items.iter().map(|t| t.get_floor_type()).collect()
+                }
+            }
+            SugaredTypeTerm::Struct { struct_repr, members } => {
+                SugaredTypeTerm::Struct {
+                    struct_repr: if let Some(sr) = struct_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    members: members.iter()
+                        .map(|SugaredStructMember{symbol,ty}|
+                            SugaredStructMember {symbol:symbol.clone(), ty:ty.get_floor_type() })
+                        .collect()
+                }
+            }
+            SugaredTypeTerm::Enum { enum_repr, variants } => {
+                SugaredTypeTerm::Enum {
+                    enum_repr: if let Some(sr) = enum_repr {
+                        Some(Box::new(sr.clone().get_floor_type()))
+                    } else { None },
+                    variants: variants.iter()
+                        .map(|SugaredEnumVariant{symbol,ty}|
+                            SugaredEnumVariant{ symbol:symbol.clone(), ty:ty.get_floor_type() })
+                        .collect()
+                }
+            }
+
+            SugaredTypeTerm::TypeID(tyid) => SugaredTypeTerm::TypeID(tyid.clone()),
+            SugaredTypeTerm::Num(n) => SugaredTypeTerm::Num(*n),
+            SugaredTypeTerm::Char(c) => SugaredTypeTerm::Char(*c)
+            */
+
+            other => (SugaredTypeTerm::unit(), other.clone().strip())
+        }
+    }
+
     pub fn is_empty(&self) -> bool {
         match self {
             SugaredTypeTerm::TypeID(_) => false,
@@ -197,16 +506,18 @@ impl SugaredTypeTerm {
             SugaredTypeTerm::Spec(ts) |
             SugaredTypeTerm::Ladder(ts) |
             SugaredTypeTerm::Func(ts) |
-            SugaredTypeTerm::Morph(ts) |
-            SugaredTypeTerm::Seq(ts) => {
+            SugaredTypeTerm::Morph(ts) => {
                 ts.iter().fold(true, |s,t| s && t.is_empty() )
             }
-            SugaredTypeTerm::Struct(ts) => {
-                ts.iter()
+            SugaredTypeTerm::Seq{ seq_repr, items } => {
+                items.iter().fold(true, |s,t| s && t.is_empty() )
+            }
+            SugaredTypeTerm::Struct{ struct_repr, members } => {
+                members.iter()
                     .fold(true, |s,member_decl| s && member_decl.ty.is_empty() )
             }
-            SugaredTypeTerm::Enum(ts) => {
-                ts.iter()
+            SugaredTypeTerm::Enum{ enum_repr, variants } => {
+                variants.iter()
                     .fold(true, |s,variant_decl| s && variant_decl.ty.is_empty() )
             }
         }

src/test/unification.rs

@@ -336,14 +336,14 @@ pub fn test_subtype_delim() {
         UnificationProblem::new_sub(vec![
 
             (
-                //given type
+                // given type
                 dict.parse("
                   < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
                 ~ < ValueSep ':' Char~Ascii~UInt8 >
                 ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
                 ").expect(""),
 
-                //expected type
+                // expected type
                 dict.parse("
                   < Seq <Seq T> >
                 ~ < ValueSep Delim T >
@@ -378,3 +378,78 @@ pub fn test_subtype_delim() {
         ))
     );
 }
+
+
+
+use crate::{sugar::*, unification_sugared::{SugaredUnificationPair, SugaredUnificationProblem}};
+
+#[test]
+fn test_list_subtype_sugared() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname("Item".into());
+
+    let subtype_constraints = vec![
+        SugaredUnificationPair::new(
+            dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect("").sugar(&mut dict),
+            dict.parse("<List~Vec Item~ReprTree>").expect("").sugar(&mut dict)
+        )
+    ];
+
+    assert_eq!(
+        SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+        Ok((
+            vec![ SugaredTypeTerm::Ladder(vec![]) ],
+            vec![
+                (dict.get_typeid(&"Item".into()).unwrap(),
+                    dict.parse("<Digit 10>~Char").unwrap().sugar(&mut dict))
+            ].into_iter().collect()
+        ))
+    );
+}
+
+
+#[test]
+pub fn test_subtype_delim_sugared() {
+    let mut dict = BimapTypeDict::new();
+
+    dict.add_varname(String::from("T"));
+    dict.add_varname(String::from("Delim"));
+
+    let subtype_constraints = vec![
+        SugaredUnificationPair::new(
+            dict.parse("
+              < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
+            ~ < ValueSep ':' Char~Ascii~UInt8 >
+            ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
+            ").expect("").sugar(&mut dict),
+
+            dict.parse("
+              < Seq <Seq T> >
+            ~ < ValueSep Delim T >
+            ~ < Seq~<LengthPrefix UInt64> T >
+            ").expect("").sugar(&mut dict),
+        ),
+        SugaredUnificationPair::new(
+            dict.parse("T").expect("").sugar(&mut dict),
+            dict.parse("UInt8").expect("").sugar(&mut dict),
+        ),
+    ];
+
+    assert_eq!(
+        SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+        Ok((
+            // halo types for each rhs in the sub-equations
+            vec![
+                dict.parse("<Seq <Seq <Digit 10>>>").expect("").sugar(&mut dict),
+                dict.parse("Char~Ascii").expect("").sugar(&mut dict),
+            ],
+
+            // variable substitution
+            vec![
+                (dict.get_typeid(&"T".into()).unwrap(), dict.parse("Char~Ascii~UInt8").expect("").sugar(&mut dict)),
+                (dict.get_typeid(&"Delim".into()).unwrap(), SugaredTypeTerm::Char(':')),
+            ].into_iter().collect()
+        ))
+    );
+}

src/unification.rs

@@ -25,16 +25,19 @@ pub struct UnificationProblem {
     σ: HashMap<TypeID, TypeTerm>,
     upper_bounds: HashMap< u64, TypeTerm >,
     lower_bounds: HashMap< u64, TypeTerm >,
+
     equal_pairs: Vec<UnificationPair>,
     subtype_pairs: Vec<UnificationPair>,
-    trait_pairs: Vec<UnificationPair>
+    trait_pairs: Vec<UnificationPair>,
+    parallel_pairs: Vec<UnificationPair>
 }
 
 impl UnificationProblem {
     pub fn new(
         equal_pairs: Vec<(TypeTerm, TypeTerm)>,
         subtype_pairs: Vec<(TypeTerm, TypeTerm)>,
-        trait_pairs: Vec<(TypeTerm, TypeTerm)>
+        trait_pairs: Vec<(TypeTerm, TypeTerm)>,
+        parallel_pairs: Vec<(TypeTerm, TypeTerm)>
     ) -> Self {
         UnificationProblem {
             σ: HashMap::new(),
@@ -60,17 +63,24 @@ impl UnificationProblem {
                     addr: Vec::new()
                 }).collect(),
 
+            parallel_pairs: parallel_pairs.into_iter().map(|(lhs,rhs)|
+                UnificationPair{
+                    lhs,rhs,
+                    halo: TypeTerm::unit(),
+                    addr: Vec::new()
+                }).collect(),
+
             upper_bounds: HashMap::new(),
             lower_bounds: HashMap::new(),
         }
     }
 
     pub fn new_eq(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
-        UnificationProblem::new( eqs, Vec::new(), Vec::new() )
+        UnificationProblem::new( eqs, Vec::new(), Vec::new(), Vec::new() )
     }
 
     pub fn new_sub(subs: Vec<(TypeTerm, TypeTerm)>) -> Self {
-        UnificationProblem::new( Vec::new(), subs, Vec::new() )
+        UnificationProblem::new( Vec::new(), subs, Vec::new(), Vec::new() )
     }
 
 
@@ -527,4 +537,12 @@ pub fn subtype_unify(
     unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
 }
 
+pub fn parallel_unify(
+    t1: &TypeTerm,
+    t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
+    let unification = UnificationProblem::new(vec![], vec![], vec![], vec![ (t1.clone(), t2.clone()) ]);
+    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
+}
+
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\

src/unification_sugared.rs

@@ -0,0 +1,686 @@
+use {
+    crate::{dict::*, sugar::SugaredTypeTerm, term::*, SugaredEnumVariant, SugaredStructMember}, std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct SugaredUnificationError {
+    pub addr: Vec<usize>,
+    pub t1: SugaredTypeTerm,
+    pub t2: SugaredTypeTerm
+}
+
+#[derive(Clone)]
+pub struct SugaredUnificationPair {
+    addr: Vec<usize>,
+    lhs: SugaredTypeTerm,
+    rhs: SugaredTypeTerm,
+}
+
+impl SugaredUnificationPair {
+    pub fn new(lhs: SugaredTypeTerm, rhs: SugaredTypeTerm) -> Self {
+        SugaredUnificationPair {
+            lhs,rhs, addr:vec![]
+        }
+    }
+}
+
+pub struct SugaredUnificationProblem {
+   // dict: &'a Dict,
+
+    σ: HashMap<TypeID, SugaredTypeTerm>,
+    upper_bounds: HashMap< u64, SugaredTypeTerm >,
+    lower_bounds: HashMap< u64, SugaredTypeTerm >,
+
+    equal_pairs: Vec<SugaredUnificationPair>,
+    subtype_pairs: Vec<SugaredUnificationPair>,
+    trait_pairs: Vec<SugaredUnificationPair>,
+    parallel_pairs: Vec<SugaredUnificationPair>
+}
+
+impl SugaredUnificationProblem {
+    pub fn new(
+       // dict: &'a mut Dict,
+        equal_pairs: Vec<SugaredUnificationPair>,
+        subtype_pairs: Vec<SugaredUnificationPair>,
+        trait_pairs: Vec<SugaredUnificationPair>,
+        parallel_pairs: Vec<SugaredUnificationPair>
+    ) -> Self {
+        SugaredUnificationProblem {
+          //  dict,
+            σ: HashMap::new(),
+
+            equal_pairs,
+            subtype_pairs,
+            trait_pairs,
+            parallel_pairs,
+
+            upper_bounds: HashMap::new(),
+            lower_bounds: HashMap::new(),
+        }
+    }
+
+    pub fn new_eq(eqs: Vec<SugaredUnificationPair>) -> Self {
+        SugaredUnificationProblem::new(  eqs, Vec::new(), Vec::new(), Vec::new() )
+    }
+
+    pub fn new_sub( subs: Vec<SugaredUnificationPair>) -> Self {
+        SugaredUnificationProblem::new( Vec::new(), subs, Vec::new(), Vec::new() )
+    }
+
+    pub fn new_trait(traits: Vec<SugaredUnificationPair>) -> Self {
+        SugaredUnificationProblem::new( Vec::new(), Vec::new(), traits, Vec::new() )
+    }
+
+    pub fn new_parallel( parallels: Vec<SugaredUnificationPair>) -> Self {
+        SugaredUnificationProblem::new(Vec::new(), Vec::new(), Vec::new(), parallels )
+    }
+
+
+    /// update all values in substitution
+    pub fn reapply_subst(&mut self) {
+        let mut new_σ = HashMap::new();
+        for (v, tt) in self.σ.iter() {
+            let mut tt = tt.clone();
+            tt.apply_subst(&self.σ);
+            //eprintln!("update σ : {:?} --> {:?}", v, tt);
+            new_σ.insert(v.clone(), tt);
+        }
+        self.σ = new_σ;
+    }
+
+
+    pub fn eval_equation(&mut self, unification_pair: SugaredUnificationPair) -> Result<(), SugaredUnificationError> {
+        match (&unification_pair.lhs, &unification_pair.rhs) {
+            (SugaredTypeTerm::TypeID(TypeID::Var(varid)), t) |
+            (t, SugaredTypeTerm::TypeID(TypeID::Var(varid))) => {
+                if ! t.contains_var( *varid ) {
+                    self.σ.insert(TypeID::Var(*varid), t.clone());
+                    self.reapply_subst();
+                    Ok(())
+                } else if t == &SugaredTypeTerm::TypeID(TypeID::Var(*varid)) {
+                    Ok(())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
+                }
+            }
+
+            (SugaredTypeTerm::TypeID(a1), SugaredTypeTerm::TypeID(a2)) => {
+                if a1 == a2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (SugaredTypeTerm::Num(n1), SugaredTypeTerm::Num(n2)) => {
+                if n1 == n2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (SugaredTypeTerm::Char(c1), SugaredTypeTerm::Char(c2)) => {
+                if c1 == c2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+
+            (SugaredTypeTerm::Ladder(a1), SugaredTypeTerm::Ladder(a2)) |
+            (SugaredTypeTerm::Spec(a1), SugaredTypeTerm::Spec(a2)) => {
+                if a1.len() == a2.len() {
+                    for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push(
+                            SugaredUnificationPair {
+                                lhs: x,
+                                rhs: y,
+                                addr: new_addr
+                            });
+                    }
+                    Ok(())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            (SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+                SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+            => {
+                // todo: unify seq reprü
+
+                if lhs_items.len() == rhs_items.len() {
+                    for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+                SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+            => {
+                // todo: unify struct repr
+
+                if lhs_members.len() == rhs_members.len() {
+                    for (i,
+                            (SugaredStructMember{ symbol: lhs_symbol, ty: lhs_ty},
+                                SugaredStructMember{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+                SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+            => {
+                // todo: unify enum repr
+
+                if lhs_variants.len() == rhs_variants.len() {
+                    for (i,
+                            (SugaredEnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+                                SugaredEnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+                    }
+                    Ok(())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            _ => Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+        }
+    }
+
+
+
+    pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: SugaredTypeTerm) -> Result<(),()> {
+
+        if new_lower_bound == SugaredTypeTerm::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(
+                SugaredUnificationPair {
+                    lhs: lower_bound.clone(),
+                    rhs: new_lower_bound.clone(),
+                    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(
+                SugaredUnificationPair{
+                    lhs: new_lower_bound,
+                    rhs: lower_bound,
+                    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: SugaredTypeTerm) -> Result<(),()> {
+        if new_upper_bound == SugaredTypeTerm::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(
+                SugaredUnificationPair {
+                    lhs: new_upper_bound.clone(),
+                    rhs: upper_bound,
+                    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: SugaredUnificationPair) -> Result<
+        // ok: halo type
+        SugaredTypeTerm,
+        // error
+        SugaredUnificationError
+    > {
+       // eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
+        match (unification_pair.lhs.clone().strip(), unification_pair.rhs.clone().strip()) {
+
+            /*
+             Variables
+            */
+
+            (t, SugaredTypeTerm::TypeID(TypeID::Var(v))) => {
+                //eprintln!("t <= variable");
+                if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
+                    Ok(SugaredTypeTerm::unit())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(v)), t2: t })
+                }
+            }
+
+            (SugaredTypeTerm::TypeID(TypeID::Var(v)), t) => {
+                //eprintln!("variable <= t");
+                if self.add_upper_subtype_bound(v, t.clone()).is_ok() {
+                    Ok(SugaredTypeTerm::unit())
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(v)), t2: t })
+                }
+            }
+
+
+            /*
+             Atoms
+            */
+            (SugaredTypeTerm::TypeID(a1), SugaredTypeTerm::TypeID(a2)) => {
+                if a1 == a2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs}) }
+            }
+            (SugaredTypeTerm::Num(n1), SugaredTypeTerm::Num(n2)) => {
+                if n1 == n2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+            (SugaredTypeTerm::Char(c1), SugaredTypeTerm::Char(c2)) => {
+                if c1 == c2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+            }
+
+            /*
+             Complex Types
+            */
+
+            (SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+                SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+            => {
+                if lhs_items.len() == rhs_items.len() && lhs_items.len() > 0 {
+                    let mut new_addr = unification_pair.addr.clone();
+                    new_addr.push(0);
+                    match self.eval_subtype( SugaredUnificationPair { addr: new_addr.clone(), lhs: lhs_items[0].clone(), rhs: rhs_items[0].clone() } ) {
+                        Ok(ψ) => Ok(SugaredTypeTerm::Seq {
+                                seq_repr: None, // <<- todo
+                                items: vec![ψ]
+                            }.strip()),
+                        Err(e) => Err(SugaredUnificationError{
+                                addr: new_addr,
+                                t1: e.t1,
+                                t2: e.t2,
+                            })
+                    }
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+                SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+            => {
+                if lhs_members.len() == rhs_members.len() {
+                    let mut halo_members = Vec::new();
+                    for (i,
+                            (SugaredStructMember{ symbol: lhs_symbol, ty: lhs_ty},
+                                SugaredStructMember{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+
+                        let ψ = self.eval_subtype( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+                        halo_members.push(SugaredStructMember { symbol: lhs_symbol, ty: ψ });
+                    }
+                    Ok(SugaredTypeTerm::Struct {
+                        struct_repr: None,
+                        members: halo_members
+                    })
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+            (SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+                SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+            => {
+                if lhs_variants.len() == rhs_variants.len() {
+                    let mut halo_variants = Vec::new();
+                    for (i,
+                            (SugaredEnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+                                SugaredEnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+                        ) in
+                            lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+                    {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+                        let ψ = self.eval_subtype( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+                        halo_variants.push(SugaredEnumVariant { symbol: lhs_symbol, ty: ψ });
+                    }
+                    Ok(SugaredTypeTerm::Enum {
+                        enum_repr: None,
+                        variants: halo_variants
+                    })
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+
+
+            /*
+             Ladders
+            */
+
+            (SugaredTypeTerm::Ladder(a1), SugaredTypeTerm::Ladder(a2)) => {
+
+                let mut l1_iter = a1.into_iter().enumerate().rev();
+                let mut l2_iter = a2.into_iter().rev();
+
+                let mut halo_ladder = Vec::new();
+
+                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);
+
+                        match (lhs.clone(), rhs.clone()) {
+                            (t, SugaredTypeTerm::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
+                                        todo!();
+
+                                    } else {
+                                        // ladder of rhs is empty
+                                        // 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, SugaredTypeTerm::Ladder(new_upper_bound_ladder)).is_ok() {
+                                        // ok
+                                    } else {
+                                        return Err(SugaredUnificationError {
+                                            addr,
+                                            t1: lhs,
+                                            t2: rhs
+                                        });
+                                    }
+                                } else {
+                                    return Err(SugaredUnificationError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
+                                }
+                            }
+                            (lhs, rhs) => {
+                                if let Ok(ψ) = self.eval_subtype(
+                                    SugaredUnificationPair {
+                                        lhs: lhs.clone(),
+                                        rhs: rhs.clone(),
+                                        addr:addr.clone(),
+                                    }
+                                ) {
+                                    // ok.
+                                    //eprintln!("rungs are subtypes. continue");
+                                    halo_ladder.push(ψ);
+                                } else {
+                                    return Err(SugaredUnificationError {
+                                        addr,
+                                        t1: lhs,
+                                        t2: rhs
+                                    });
+                                }
+                            }
+                        }
+                    } else {
+                        // not a subtype,
+                        return Err(SugaredUnificationError {
+                            addr: vec![],
+                            t1: unification_pair.lhs,
+                            t2: unification_pair.rhs
+                        });
+                    }
+                }
+                //eprintln!("left ladder fully consumed");
+
+                for (i,t) in l1_iter {
+                    //!("push {} to halo ladder", t.pretty(self.dict,0));
+                    halo_ladder.push(t);
+                }
+                halo_ladder.reverse();
+                Ok(SugaredTypeTerm::Ladder(halo_ladder).strip())//.param_normalize())
+            },
+
+            (t, SugaredTypeTerm::Ladder(a1)) => {
+                Err(SugaredUnificationError{ addr: unification_pair.addr, t1: t, t2: SugaredTypeTerm::Ladder(a1) })
+            }
+
+            (SugaredTypeTerm::Ladder(mut a1), t) => {
+                if a1.len() > 0 {
+                    let mut new_addr = unification_pair.addr.clone();
+                    new_addr.push( a1.len() -1 );
+                    if let Ok(halo) = self.eval_subtype(
+                        SugaredUnificationPair {
+                            lhs: a1.pop().unwrap(),
+                            rhs: t.clone(),
+                            addr: new_addr
+                        }
+                    ) {
+                        a1.push(halo);
+                        if a1.len() == 1 {
+                            Ok(a1.pop().unwrap())
+                        } else {
+                            Ok(SugaredTypeTerm::Ladder(a1))
+                        }
+                    } else {
+                        Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::Ladder(a1), t2: t })
+                    }
+                } else if t == SugaredTypeTerm::unit() {
+                    Ok(SugaredTypeTerm::unit())
+                } else {
+                    Err(SugaredUnificationError { addr: unification_pair.addr, t1: SugaredTypeTerm::unit(), t2: t })
+                }
+            }
+
+
+            /*
+             Application
+            */
+
+            (SugaredTypeTerm::Spec(a1), SugaredTypeTerm::Spec(a2)) => {
+                if a1.len() == a2.len() {
+                    let mut halo_args = Vec::new();
+                    let mut n_halos_required = 0;
+
+                    for (i, (mut x, mut y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+                        let mut new_addr = unification_pair.addr.clone();
+                        new_addr.push(i);
+
+                        x = x.strip();
+
+//                        eprintln!("before strip: {:?}", y);
+                        y = y.strip();
+//                        eprintln!("after strip: {:?}", y);
+//                        eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
+
+                        match self.eval_subtype(
+                            SugaredUnificationPair {
+                                lhs: x.clone(),
+                                rhs: y.clone(),
+                                addr: new_addr,
+                            }
+                        ) {
+                            Ok(halo) => {
+                                if halo == SugaredTypeTerm::unit() {
+                                    let mut y = y.clone();
+                                    y.apply_subst(&self.σ);
+                                    y = y.strip();
+
+                                    let top = y.get_interface_type();
+                                    // eprintln!("add top {}", top.pretty(self.dict, 0));
+                                    halo_args.push(top);
+                                } else {
+                                    //println!("add halo {}", halo.pretty(self.dict, 0));
+                                    if n_halos_required > 0 {
+                                        let x = &mut halo_args[n_halos_required-1];
+                                        if let SugaredTypeTerm::Ladder(arg_rungs) = x {
+                                            let mut a = a2[n_halos_required-1].clone();
+                                            a.apply_subst(&self.σ);
+                                            arg_rungs.push(a.get_interface_type());
+                                        } else {
+                                            *x = SugaredTypeTerm::Ladder(vec![
+                                                x.clone(),
+                                                a2[n_halos_required-1].get_interface_type()
+                                            ]);
+
+                                            x.apply_subst(&self.σ);
+                                        }
+                                    }
+
+                                    halo_args.push(halo);
+                                    n_halos_required += 1;
+                                }
+                            },
+                            Err(err) => { return Err(err); }
+                        }
+                    }
+
+                    if n_halos_required > 0 {
+                        //eprintln!("halo args : {:?}", halo_args);
+                        Ok(SugaredTypeTerm::Spec(halo_args))
+                    } else {
+                        Ok(SugaredTypeTerm::unit())
+                    }
+                } else {
+                    Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+                }
+            }
+
+            _ => Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+        }
+    }
+
+    pub fn solve(mut self) -> Result<(Vec<SugaredTypeTerm>, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+        // solve equations
+        while let Some( mut equal_pair ) = self.equal_pairs.pop() {
+            equal_pair.lhs.apply_subst(&self.σ);
+            equal_pair.rhs.apply_subst(&self.σ);
+
+            self.eval_equation(equal_pair)?;
+        }
+
+        // solve subtypes
+//        eprintln!("------ SOLVE SUBTYPES ---- ");
+        for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+            subtype_pair.lhs.apply_subst(&self.σ);
+            subtype_pair.rhs.apply_subst(&self.σ);
+            let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+        }
+
+        // add variables from subtype bounds
+        for (var_id, t) in self.upper_bounds.iter() {
+//            eprintln!("VAR {} upper bound {:?}", var_id, t);
+            self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+        }
+
+        for (var_id, t) in self.lower_bounds.iter() {
+//            eprintln!("VAR {} lower bound {:?}", var_id, t);
+            self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+        }
+
+        self.reapply_subst();
+
+//        eprintln!("------ MAKE HALOS -----");
+        let mut halo_types = Vec::new();
+        for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+            subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone().strip();
+            subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone().strip();
+
+            subtype_pair.lhs.apply_subst(&self.σ);
+            subtype_pair.rhs.apply_subst(&self.σ);
+
+           // eprintln!("find halo.\n lhs={}", subtype_pair.lhs.pretty(self.dict,0));
+           // eprintln!("rhs={}", subtype_pair.rhs.pretty(self.dict,0));
+
+            let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+            halo_types.push(halo);
+        }
+
+        // solve traits
+        while let Some( trait_pair ) = self.trait_pairs.pop() {
+            unimplemented!();
+        }
+
+        Ok((halo_types, self.σ))
+    }
+}
+
+pub fn unify(
+    t1: &SugaredTypeTerm,
+    t2: &SugaredTypeTerm
+) -> Result<HashMap<TypeID, SugaredTypeTerm>, SugaredUnificationError> {
+    let unification = SugaredUnificationProblem::new_eq(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    Ok(unification.solve()?.1)
+}
+
+pub fn subtype_unify(
+    t1: &SugaredTypeTerm,
+    t2: &SugaredTypeTerm
+) -> Result<(SugaredTypeTerm, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+    let unification = SugaredUnificationProblem::new_sub(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(SugaredTypeTerm::unit()), σ) )
+}
+
+pub fn parallel_unify(
+    t1: &SugaredTypeTerm,
+    t2: &SugaredTypeTerm
+) -> Result<(SugaredTypeTerm, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+    let unification = SugaredUnificationProblem::new_parallel(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+    unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(SugaredTypeTerm::unit()), σ) )
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\