idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 368 forks source link

[ fix ] Fix search around `%defaulthints` #3258

Closed buzden closed 2 weeks ago

buzden commented 2 months ago

Fixes #2850, fixes #2932.

The root cause of both fixed problems was errorneous proparation of the defaults flag down to search of dependencies of found hint candidates. Default hint may require non-default implementation as an auto-argument and vice versa. You can see cases in reported issues being fixed.

Some special error treatement was added to make sure we leave adequate error messages in case of the whole search went bad.

This PR is split to several commits to make review easier.