Hi,

I'm puzzled about the type error returned with the following code (fix :
remove "fs"). Assuming value "mgu" and constructor "Var" are defined, is
it reasonable to report a type error about "subst" rather than the
unbound value "fs" ? I would expect the type-checker to first
successfully type the folded function, (with type (var_name * term) list
-> var_name * term -> (var_name * term) list) and then complain about
unbound value fs.

Tiphaine

let genereal_unify subst eqs =
  List.fold_left (fun subst (x, t) -> mgu subst (Var x) t) subst fs eqs

File "prolog.ml", line 475, characters 42-47: (* i.e., second occurrence
of subst *))
Error: This expression has type 'a -> 'b but is here used with type
         (var_name * term) list