Importing seemingly irrelevant module increases type checking time by an order of magnitude

[nicolabotta]

I came across another odd behavior of the type checker that makes it effectively impossible for me to write application-level code in Idris. The program

https://gitlab.pik-potsdam.de/botta/IdrisLibs/blob/master/issues/type_checking_times.lidr

type checks fine. On a fresh IdrisLibs installation, you should be able to do

cd issues/
idris -i .. -i ../.. --sourcepath .. --sourcepath ../.. --check -V type_checking_times.lidr
rm type_checking_times.ibc
time idris -i .. -i ../.. --sourcepath .. --sourcepath ../.. --check -V type_checking_times.lidr

and see type checking times of about one minute. This is a bit slow but still acceptable. However, uncommenting import SequentialDecisionProblems.Utils at line 7 yields

rm type_checking_times.ibc
time idris -i .. -i ../.. --sourcepath .. --sourcepath ../.. --check -V type_checking_times.lidr
Type checking ./type_checking_times.lidr
type_checking_times.lidr:46:3:
SequentialDecisionProblems.CoreTheory.nexts is not total as there are missing cases

real    24m10.834s
user    10m5.764s
sys 2m35.480s

Here we are already at half an hour type cheking time although all I have done is importing a module that is not needed for the actual code. Notice that type checking the imported module itself takes about 10 seconds. The additional 24 minutes are spent type checking the implementation of the nexts function at lines 46-85 of type_checking_times.lidr!

Why does importing a module that is actually not used and type checks in 10 seconds increase the type checking time by a factor 20?

Notice that adding one more pattern to the implementation of nexts makes type checking practically impossible: the Idris process starts swapping and eventually stalls. On the other hand, if SequentialDecisionProblems.Utils is not imported, adding one more pattern to the implementation of nexts increases the type cheking time from one to two minutes as one would expect.

Edit: I realized that I have another open issue with the same title. Perhaps this one should be renamed to "Type checking times again and again!"

[ahmadsalim]

@nicolabotta Thanks for reporting the issue. I will update the title.

[ahmadsalim]

@nicolabotta Note: I think this is quite a pathological case you have here. Have you tried using top-level clauses instead of nested 'case' expressions, and is there a difference in erformance?

[nicolabotta]

No but having the computation done in let clauses completely avoids the problem. Reimplementing nextsas

> SequentialDecisionProblems.CoreTheory.nexts t (e, True, False, True) False =
>   let ttres = mkSimpleProb 
>               [((weaken e, False, False,  True),        pLH  * (one - pA1) *        pS1), 
>                ((    FS e,  True, False,  True), (one - pLH) * (one - pA1) *        pS1),
>                ((weaken e, False,  True,  True),        pLH  *        pA1  *        pS1), 
>                ((    FS e,  True,  True,  True), (one - pLH) *        pA1  *        pS1),
>                ((weaken e, False, False, False),        pLH  * (one - pA1) * (one - pS1)), 
>                ((    FS e,  True, False, False), (one - pLH) * (one - pA1) * (one - pS1)),
>                ((weaken e, False,  True, False),        pLH  *        pA1  * (one - pS1)), 
>                ((    FS e,  True,  True, False), (one - pLH) *        pA1  * (one - pS1))] in
>   let tfres = mkSimpleProb 
>               [((weaken e, False, False,  True),        pLH  * (one - pA1) *        pS2), 
>                ((    FS e,  True, False,  True), (one - pLH) * (one - pA1) *        pS2),
>                ((weaken e, False,  True,  True),        pLH  *        pA1  *        pS2), 
>                ((    FS e,  True,  True,  True), (one - pLH) *        pA1  *        pS2),
>                ((weaken e, False, False, False),        pLH  * (one - pA1) * (one - pS2)), 
>                ((    FS e,  True, False, False), (one - pLH) * (one - pA1) * (one - pS2)),
>                ((weaken e, False,  True, False),        pLH  *        pA1  * (one - pS2)), 
>                ((    FS e,  True,  True, False), (one - pLH) *        pA1  * (one - pS2))] in
>   let ftres = mkSimpleProb 
>               [((weaken e, False, False,  True),        pLH  * (one - pA2) *        pS1), 
>                ((    FS e,  True, False,  True), (one - pLH) * (one - pA2) *        pS1),
>                ((weaken e, False,  True,  True),        pLH  *        pA2  *        pS1), 
>                ((    FS e,  True,  True,  True), (one - pLH) *        pA2  *        pS1),
>                ((weaken e, False, False, False),        pLH  * (one - pA2) * (one - pS1)), 
>                ((    FS e,  True, False, False), (one - pLH) * (one - pA2) * (one - pS1)),
>                ((weaken e, False,  True, False),        pLH  *        pA2  * (one - pS1)), 
>                ((    FS e,  True,  True, False), (one - pLH) *        pA2  * (one - pS1))] in
>   let ffres = mkSimpleProb 
>               [((weaken e, False, False,  True),        pLH  * (one - pA2) *        pS2), 
>                ((    FS e,  True, False,  True), (one - pLH) * (one - pA2) *        pS2),
>                ((weaken e, False,  True,  True),        pLH  *        pA2  *        pS2), 
>                ((    FS e,  True,  True,  True), (one - pLH) *        pA2  *        pS2),
>                ((weaken e, False, False, False),        pLH  * (one - pA2) * (one - pS2)), 
>                ((    FS e,  True, False, False), (one - pLH) * (one - pA2) * (one - pS2)),
>                ((weaken e, False,  True, False),        pLH  *        pA2  * (one - pS2)), 
>                ((    FS e,  True,  True, False), (one - pLH) *        pA2  * (one - pS2))] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres

make the example type checks in about 30 seconds, no matter whether SequentialDecisionProblems.Utils is imported or not. I have no idea what is going on here but there seems to be something in the module system that makes type checking very brittle. For instance, the time it takes to type check the original implementation can also be very much reduced if one uses local versions of State, Ctrl and nexts instead of the imported ones. Very strange.