refactor(kernel/normalizer): normalizer only needs read access to metavariable environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi