search

idris-lang / Idris2

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

Performance issue with `Range` and `auto` search #1615

Open fabianhjr opened 3 years ago

fabianhjr commented 3 years ago

Steps to Reproduce

Time the test case from #1581 with #1602

Expected Behavior

Typecheck quickly

Observed Behavior

> time idris2 --check test.idr
1/1: Building test (test.idr)

________________________________________________________
Executed in    8.45 secs    fish           external
   usr time    8.32 secs    0.00 micros    8.32 secs
   sys time    0.12 secs  335.00 micros    0.11 secs
edwinb commented 3 years ago

This is because of the auto implicit which normalises the goal before starting, in order to check that the determining arguments have a concrete value. We need this because auto search isn't allowed to solve holes in determining arguments. As things stand, the rules say there must be no holes at all in the value, which involves fully normalising. Making the range functions public means that the evaluator needs to do a lot more work to get to the normal form.

So, I'm not surprised this happens, in the end. We can make it go quite a bit quicker by switching to CBV evaluation - and that's just a flag to the evaluator, so I might do that for auto search since it needs a normal form - but in general you will see this behaviour for auto search.