Records the history of currently open implicit searches.
A search history maintains a list of open implicit searches (
open) a shortcut flag
indicating whether any of these are by name (
byname) and a reference to the root
search history (
root) which in turn maintains a possibly empty dictionary of
recursive implicit terms constructed during this search.
A search history provides operations to create a nested search history, check for divergence, enter by name references and definitions in the implicit dictionary, lookup recursive references and emit a complete implicit dictionary when the outermost search is complete.
Does this search history contain any by name implicit arguments.
Check if the supplied candidate implicit and target type indicate a diverging implicit search.
Create the state for a nested implicit search.
Return the reference, if any, to a term under construction or already constructed in the current search history corresponding to the supplied target type.
A term is eligible if its type is a subtype of the target type and either it has already been constructed and is present in the current implicit dictionary, or it is currently under construction and is separated from the current search context by at least one by name argument position.
Note that because any suitable term found is defined as part of this search it will always be effectively in a more inner context than any other definition provided by explicit definitions. Consequently these terms have the highest priority and no other candidates need to be considered.