Visibility in elaboration scripts requires doing strange stuff

[buzden]

This simple elaboration script and code running it typecheks fine (requires contrib library).

import Data.SortedSet
import Data.SortedMap
import Data.SortedMap.Dependent

import Language.Reflection

%language ElabReflection

scr : List Nat -> Elab Unit
scr xs = ignore $ logMsg "debug" 0 "length: \{show $ length $ SortedSet.toList $ fromList xs}"

%runElab scr [0, 2, 3]

However, one may notice that no SortedMap-related stuff are present in the code.

Steps to Reproduce

Remove import Data.SortedMap and import Data.SortedMap.Dependent

Expected Behavior

All continues to typecheck.

Observed Behavior

Error: Can't reify as String

Comments

To understand what's going on, it's important to understand that in contrib SortedSet from Data.SortedSet is implemented through SortedMap from Data.SortedMap and SortedMap is implemented through SortedDMap from Data.SortedMap.Dependent. No functions are exported publicly from these modules. All visible functions (e.g. fromList and toList) are export and are implemented through several private functions.

Elaboration scripts are "executed" at compile-time through evaluation the script value and interpreting it with ongoing reduction of all functions that are met on the way during this interpretation. Definitions of non-public functions are available during this process (in either way only public functions could be used in elaboration scripts, which is extremely limiting).

The problem is that somewhy the module which contains those non-public functions whose bodies are used in reduction during interpretation must be imported in the context of the running point of the elaboration script. It means that if elaboration script is used in another module, module that defines elaboration script should not only import all the modules with used functions deeply, but it also should import public them. This is annoying and fragile since to use an elaboration script successfully, I must know implementation of all the stuff that is used by this elaboration script (or the author of the script must know it and import public everything down).

BTW, as far as I remember, this is related to #1955 and #1946.