Visibility workaround for #1946

[berewt]

While it doesn't solve #1946 issue per say, it allows at least the issue examples to pass:
if we publicly export Language.Reflection.check, the reducibleInAll check of Core.Normalize.Eval.eval pass to true and check is translated into Check in all cases.
I still don't get why we don't need this public export in some cases, but we may figure it out later.

[buzden]

Well, I have a still unreported but similarly worked around elab-related problem. For example, when in my elaboration scripts I use something, that's needed to be imported, say Data.SortedSet, I have to do import public Data.SortedSet in the module where the elaboration script defined, or I get the "stuck function" problem in seemingly arbitrary places.

[berewt]

I still have to take some time to investigate why check behaves differently under a lambda. We probably need a more precise condition to decide whether we should try to evaluate a term or not, but it’s hard (with my current knowledge at least) to understand how and when.