feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'

This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/normalizer): provide the metavar_env to instantiate and add_inst in the normalizer, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed

The modifications started at commit 1852c86948dd7da8a2bac224e3c7c0ee309db224 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): provide the metavar_env to instantiate and lift_free_vars in the elaborator, it will minimize the number of local_entries needed