Idris2
Idris2 copied to clipboard
"Ambiguous elaboration" when only one option type checks
I regularly come across "Ambiguous elaboration", followed by a number of options. When I disambiguate to each of these options, only one type checks. I would consider this a bug since it's not ambiguous if only one option is valid.
I don't have a minimal example to provide. My current example relies on a very complex environment and would be tricky to disentangle. I feel this is such a common error that perhaps these can be added later. Correct me if that's not true.