Slight difference with Haskell version in substitution

[hawnzug]

In the post Simpler, Easier!, in the case of substituting lambda and pi, when the bound variable coincide with v, it leaves the expression untouched but still substitute in the type.

subst :: Sym -> Expr -> Expr -> Expr
subst v x = sub
  where sub (Lam i t e) = abstr Lam i t e
        sub (Pi i t e) = abstr Pi i t e
        abstr con i t e =
            if v == i then
                con i (sub t) e

But in Rust version it simply keeps everything untouched.

if bound == from {
    self.clone()
}

I'm new to pure type system so I'm not sure which version is correct but I think the Haskell version is more consistent with the process of finding free variables, which first removes the occurrence of bounded variable in inner part, then union the free variables in type. Would you take some time to review this part?

[AndyShiue]

You are right. The variable shouldn't be bound in its type.

[AndyShiue]

Should be fixed.