Record the list of variables with their types in typing rules ?

[fblanqui]

This field would be set after checking subjection reduction. This would simplify termination and confluence checking. Note that it is important that termination and confluence checking is fast. Otherwise people won't use it.

[rlepigre]

Note that this is going to be very tricky, and it is not even clear what the type of a pattern variable is. Or is it? What about constraints for example?