Modified elaboration of terms with meta-variables: one should only -infer- types and never check, as some of the meta-vars can be unresolved at that point.

Checking may be done after the elaboration phase, when the mvars have been substituted.