Minimal example: loading QuantifiedLanguage into ghci, and attempting to match φ(τ) with P(f(a)) via folMatch (phi1 1 $ tau 1) $ pred "P" $ fn "f" $ cn "a" results in the substitutions {φ → λα.P(α),τ → f(a)}, and {φ → λα.P(f(a))}, but not {τ → a,φ → λ α. P(f(α))}.
Downstream, this makes certain quantifier inferences that should be correct come out incorrect.
Minimal example: loading QuantifiedLanguage into ghci, and attempting to match φ(τ) with P(f(a)) via
folMatch (phi1 1 $ tau 1) $ pred "P" $ fn "f" $ cn "a"results in the substitutions {φ → λα.P(α),τ → f(a)}, and {φ → λα.P(f(a))}, but not {τ → a,φ → λ α. P(f(α))}.Downstream, this makes certain quantifier inferences that should be correct come out incorrect.