"Can't verify injectivity" error about idris-dev HOT 2 CLOSED

I've worked out what's going on here - simply that elaboration happens in the wrong order, so when applying lemmaC3 it doesn't yet know that the p argument has to be reachable - but I'm not totally happy with my solution to it even though all the tests pass and libraries build...

There was previously a bit of a hack on elaboration order of arguments, to do arguments that informed the rest of elabroation most, earlier, but now it's a bit cleverer about postponing unification problems, I'm not sure it's necessary.

I have pushed a patch - let me know if it breaks anything else (it doesn't for me though).

from idris-dev.

Edwin Brady [email protected] wrote:

I have pushed a patch - let me know if it breaks anything else (it
doesn't for me though).

Edwin,

so far everything seems to work very nicely, thanks !

I'm still at home with a bad cold but I'll go back to the real code asap
and check the impact of the new improvements.

I still have not opened an issue on the linear vs exponential complexity
problem because I thought it was of a somehow different nature. If you
like me to do so, please let me know.

Best,
Nicola

from idris-dev.