diff --git a/src/morphism.rs b/src/morphism.rs
index ba7cc23..52e14e7 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -193,10 +193,11 @@ impl<M: Morphism + Clone> MorphismBase<M> {
 
         // try to find primitive morphism
         for m in self.morphisms.iter() {
+            eprintln!("check morphism {:?}", m.get_type());
             let unification_problem = UnificationProblem::new(
                 vec![
-                    ( ty.src_type.clone().normalize(), m.get_type().src_type.clone() ),
-                    ( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone() )
+                    ( ty.src_type.clone().normalize(), m.get_type().src_type.clone().normalize() ),
+                    ( ty.dst_type.clone().normalize(), m.get_type().dst_type.clone().normalize() )
                 ]
             );
 
diff --git a/src/pnf.rs b/src/pnf.rs
index 4576be5..54f2f5f 100644
--- a/src/pnf.rs
+++ b/src/pnf.rs
@@ -2,6 +2,20 @@ use crate::term::TypeTerm;
 
 //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
 
+pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm >  ) -> Vec< TypeTerm > {
+    for i in 0 .. upper.len() {
+        if upper[i] == lower[0] {
+            let mut result_ladder = Vec::<TypeTerm>::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 TypeTerm {
     /// transmute type into Parameter-Normal-Form (PNF)
     ///
@@ -14,84 +28,76 @@ impl TypeTerm {
         match self {
             TypeTerm::Ladder(mut rungs) => {
                 if rungs.len() > 0 {
-                    // normalize all rungs separately
-                    for r in rungs.iter_mut() {
-                        *r = r.clone().param_normalize();
-                    }
+                    let mut new_rungs = Vec::new();
+                    while let Some(bottom) = rungs.pop() {
+                        if let Some(last_but) = rungs.last_mut() {
+                            match (bottom, last_but) {
+                                (TypeTerm::App(bot_args), TypeTerm::App(last_args)) => {
+                                    if bot_args.len() == last_args.len() {
+                                        let mut different_idx = None;
+                                        let mut new_rung_params = Vec::new();
 
-                    // take top-rung
-                    match rungs.remove(0) {
-                        TypeTerm::App(params_top) => {
-                            let mut params_ladders = Vec::new();
-                            let mut tail : Vec<TypeTerm> = Vec::new();
+                                        let mut require_break = false;
 
-                            // append all other rungs to ladders inside
-                            // the application
-                            for p in params_top {
-                                params_ladders.push(vec![ p ]);
-                            }
+                                        for i in 0 .. bot_args.len() {
+                                            if let Ok(rung_idx) = bot_args[i].is_syntactic_subtype_of(&last_args[i]) {
+                                                let spliced_type_ladder = splice_ladders(
+                                                    last_args[i].clone().get_lnf_vec(),
+                                                    bot_args[i].clone().get_lnf_vec()
+                                                );
 
-                            for r in rungs {
-                                match r {
-                                    TypeTerm::App(mut params_rung) => {
-                                        if params_rung.len() > 0 {
-                                            let mut first_param = params_rung.remove(0); 
+                                                let spliced_type =
+                                                    if spliced_type_ladder.len() == 1 {
+                                                        spliced_type_ladder[0].clone()
+                                                    } else if spliced_type_ladder.len() > 1 {
+                                                        TypeTerm::Ladder(spliced_type_ladder)
+                                                    } else {
+                                                        TypeTerm::unit()
+                                                    };
 
-                                            if first_param == params_ladders[0][0] {
-                                               for (l, p) in params_ladders.iter_mut().skip(1).zip(params_rung) {
-                                                   l.push(p.param_normalize());
-                                               }
+                                                new_rung_params.push( spliced_type.param_normalize() );
                                             } else {
-                                               params_rung.insert(0, first_param);
-                                               tail.push(TypeTerm::App(params_rung));
+                                                if different_idx.is_none() {
+                                                    let spliced_type = TypeTerm::Ladder(vec![
+                                                        last_args[i].clone(),
+                                                        bot_args[i].clone()
+                                                    ]);
+                                                    new_rung_params.push( spliced_type.param_normalize() );
+                                                    different_idx = Some(i);
+                                                } else {
+                                                    require_break = true;
+                                                }
                                             }
                                         }
-                                    }
 
-                                    TypeTerm::Ladder(mut rs) => {
-                                        for r in rs {
-                                            tail.push(r.param_normalize());
+                                        if require_break {
+                                            new_rungs.push( TypeTerm::App(new_rung_params) );
+                                        } else {
+                                            rungs.pop();
+                                            rungs.push(TypeTerm::App(new_rung_params));
                                         }
-                                    }
 
-                                    atomic => {
-                                        tail.push(atomic);
+                                    } else {
+                                        new_rungs.push( TypeTerm::App(bot_args) );
                                     }
                                 }
+                                (bottom, last_buf) => {
+                                    new_rungs.push( bottom );
+                                }
                             }
-
-                            let head = TypeTerm::App(
-                                params_ladders.into_iter()
-                                    .map(
-                                        |mut l| {
-                                            l.dedup();
-                                            match l.len() {
-                                                0 => TypeTerm::unit(),
-                                                1 => l.remove(0),
-                                                _ => TypeTerm::Ladder(l).param_normalize()
-                                            }
-                                        }
-                                    )
-                                    .collect()
-                            );
-
-                            if tail.len() > 0 {
-                                tail.insert(0, head);
-                                TypeTerm::Ladder(tail)
-                            } else {
-                                head
-                            }
+                        } else {
+                            new_rungs.push( bottom );
                         }
+                    }
 
-                        TypeTerm::Ladder(mut r) => {
-                            r.append(&mut rungs);
-                            TypeTerm::Ladder(r)
-                        }
+                    new_rungs.reverse();
 
-                        atomic => {
-                            rungs.insert(0, atomic);
-                            TypeTerm::Ladder(rungs)
-                        }
+                    if new_rungs.len() > 1 {
+                        TypeTerm::Ladder(new_rungs)
+                    } else if new_rungs.len() == 1 {
+                        new_rungs[0].clone()
+                    } else {
+                        TypeTerm::unit()
                     }
                 } else {
                     TypeTerm::unit()
diff --git a/src/test/pnf.rs b/src/test/pnf.rs
index 6c26823..4f04409 100644
--- a/src/test/pnf.rs
+++ b/src/test/pnf.rs
@@ -19,6 +19,11 @@ fn test_param_normalize() {
         dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
     );
 
+    assert_eq!(
+        dict.parse("<A~Y B>").expect("parse error"),
+        dict.parse("<A B>~<Y B>").expect("parse error").param_normalize(),
+    );
+
     assert_eq!(
         dict.parse("<A B~C D~E>").expect("parse error"),
         dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").param_normalize(),
@@ -30,16 +35,21 @@ fn test_param_normalize() {
     );
 
     assert_eq!(
-        dict.parse("<A~Y B>").expect("parse error"),
-        dict.parse("<A B>~<Y B>").expect("parse error").param_normalize(),
+        dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~x86.UInt8>").expect("parse error").param_normalize(),
+        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
+    );
+    assert_eq!(
+        dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> x86.UInt8>").expect("parse error").param_normalize(),
+        dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
     );
 
     assert_eq!(
-        dict.parse("<A <B C~D~E> F~G H H>").expect("parse error"),
+        dict.parse("<A~Y <B C~D~E> F~G H H>").expect("parse error"),
         dict.parse("<A <B C> F H H>
                    ~<A <B D> F H H>
                    ~<A <B E> F H H>
-                   ~<A <B E> G H H>").expect("parse errror")
+                   ~<A <B E> G H H>
+                   ~<Y <B E> G H H>").expect("parse errror")
                .param_normalize(),
     );
 }