huge commit regarding coercions to funclass and eat_prods. before there was a
so broken behaviour that is impossible to describe the changes.
now:
eat_prods he hety args
starts checking if hety is metaclosed, if it is does nothing, if not
unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
if this unification fails, does nothing (all coercions are in the
second phase.
continues eating prods in hety and args in parallel, if there is an arg
and no more prods, tries to fix the arity of (he already_processed_args).
fix_arity gives a range of possible coercions to funclass s.t.
(c (he ..)) : FunType. The eat prods and args continues, eting the remaining
args toghether with FunType. If it fails, it continues with another c to
another FunType. This recursively (yes, it backtracks. no strong opinion
here, but there is no sane heuristinc to chose one FunType).
the code is reduced to 1/3, but Localization of errors probably need fixing.