Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

"Ambiguous elaboration" when only one option type checks

Open joelberkeley opened this issue 2 years ago • 0 comments

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.

joelberkeley avatar Jul 05 '22 19:07 joelberkeley