stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
76 stars 16 forks source link

[ error ] Refine error message of `lookupName` in one particular case #76

Closed buzden closed 6 months ago

buzden commented 6 months ago

Currently, in the case of ambuguity when no local names are present, the error is wrong. Say, I have both Data.List.Quantifiers.Right and Prelude.Right in the context, and I'm in the module X. If I do lookupName `{Right}, now I get X.Right is not in scope, but I should have an ambiguity error message instead.

So, it means that logic of refined and un-refined search differs in the produced error messages. That's why I propose to replace old assert_total call to the same function with the call to the similar, but different function.

stefan-hoeck commented 6 months ago

Thanks!