remove pattern.ident.type_vars

It was not serving any good purpose, and was interfering with proofs.
Any type variable that appears in an identifier's arguments will
either (a) show up in the type of the identifier, (b) show up in
another type somewhere else in the pattern, or (c) not be needed to
well-type anything that is not an argument to that identifier.  (There
is actually a case (d), where the type variable shows up in the
arguments to another identifier but no-where else, but I'll get to
that in a moment.)  In case (a), the type-unification will pick it up
automatically.  In case (b), pattern-type unification elsewhere will
pick up that type variable.  And in case (c), it is the responsibility
of the function that describes the arguments to the identifier to
handle any dependencies.  Case (d), where there is non-linear matching
on identifier type-arguments, is now forbidden; we will allow the
author of the rewrite-rule to deal with such equalities manually.
This allows some proofs about type unification to actually go through
now.

0 files changed, 0 insertions, 0 deletions