morphism instance: fix apply subst

src/morphism_sugared.rs

@@ -330,10 +330,21 @@ impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
     }
 
     pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, SugaredTypeTerm >) {
+        let ty = self.get_type();
         match self {
             MorphismInstance2::Primitive { ψ, σ, morph } => {
-                ψ.apply_subst(σ);
-                *σ = σ.clone().append(γ);
+                ψ.apply_subst(γ);
+                for (n,t) in σ.iter_mut() {
+                    t.apply_subst(γ);
+                }
+                for (n,t) in γ.iter() {
+                    if let TypeID::Var(varid) = n {
+                        if morph.get_type().src_type.apply_subst(σ).contains_var(*varid)
+                        || morph.get_type().dst_type.apply_subst(σ).contains_var(*varid) {
+                            σ.insert(n.clone(), t.clone());
+                        }
+                    }
+                }
             },
             MorphismInstance2::Chain { path } => {
                 for n in path.iter_mut() {