Option to increase performance: do not filter out absurd clauses automatically

[andreasabel]

Agda 2.6.0 saw an UX improvement: Agda could now filter out missing clauses (in case splitting and coverage checking) that could be shown absurd by further splittings.

• Make absurd patterns not needed at toplevel #1086 fixed in h242684bca62fabe43e125aefae7526be4b26a135
• Do not generate trivially impossible clause when case-splitting #3526 fixed in [ fix #3526 ] Remove trivially impossible clauses from case-split #3533

However, @oskeri reports a 33% typechecker speedup for one of his Agda files (from 30sec to 20sec) by inserting the absurd clauses manually.

Consequently, the user should be able to opt out this potentially expensive аппара́тчик.
I suggest a new option --performance:absurd-clauses.
This option would switch off the step in the coverage checker that filters said absurd clauses. Consequently, the respective step in the interactive case splitting should be switched off at the same time.

Relevant code to disable by this option:

agda/src/full/Agda/TypeChecking/Coverage.hs

Lines 170 to 174 in bb3602f

	-- filter out the missing clauses that are absurd.
	pss <- flip filterM pss $ \(tel,ps) ->
	-- Andreas, 2019-04-13, issue #3692: when adding missing absurd
	-- clauses, also put the absurd pattern in.
	caseEitherM (checkEmptyTel noRange tel) (\ _ -> return True) $ \ l -> do

agda/src/full/Agda/Interaction/MakeCase.hs

Lines 416 to 420 in bb3602f

	-- trivially empty clause due to the refined patterns
	else
	ifM (liftTCM $ isEmptyTel (scTel sc))
	{- then -} (pure Nothing)
	{- else -} (Just <$> makeAbstractClause f rhs ell' sc)

[nad]

This makes sense to me. However, the flag does not only affect performance, it also affects semantics, so I don't think it should be called --performance:absurd-clauses.

[andreasabel]

This makes sense to me. However, the flag does not only affect performance, it also affects semantics, so I don't think it should be called --performance:absurd-clauses.

Ah, I already wondered about the absence of bikeshedding, since I read your comment on #6435 first. Now the world is back in its usual state... ;-) Let's discuss the name at #6435.

[nad]

Have you tried to type-check the standard library with --no-infer-absurd-clauses?

• What number of files fail without {-# OPTIONS --infer-absurd-clauses #-}?
• Does the change lead to a noticeable speedup?

[andreasabel]

Good questions. I would assume the speedup is noticeable if you have complicated left-hand sides.
I think it is worthwhile checking this for the standard library, once it got past the 2.6.3 release.

[nad]

Would an alternative to this option be to infer absurd clauses only if the coverage checker complains? (Perhaps this can be implemented in a smart way without too much recomputation.) In that case one could perhaps get a speedup without having to use this flag.

The flag --no-infer-absurd-clauses could still be used to ensure that Agda never attempts the potentially slow absurd clause inference.

[nad]

Would an alternative to this option be to infer absurd clauses only if the coverage checker complains? (Perhaps this can be implemented in a smart way without too much recomputation.)

Or is this what is currently implemented (more or less)? In that case I would not expect that the standard library experiment that I suggested above (adding --infer-absurd-clauses only to those files that would fail without this option) would lead to a noticeable speedup.

[andreasabel]

Well if the coverage checker finds uncovered lhss, it tries to discharge them as absurd.

[MatthewDaggitt]

The standard library does now make use of this feature, with it being particularly useful in Data.Int.Properties as far as I remember. Therefore just a heads up that I don't think it will type-check with this flag on.

[nad]

For my library equality I got the following numbers:

• Inference of absurd clauses was used in 24 out of 220 Agda files.
• Typechecking times without any changes (two runs, I used --ignore-interfaces --profile=modules as well as +RTS -s -M4.5G):

  Total   time  655.770s  (654.070s elapsed)
  Total   time  667.649s  (665.680s elapsed)
  

• With --no-infer-absurd-clauses, but --infer-absurd-clauses turned on locally in the 24 files (plus another file in which it was not needed):

  Total   time  684.181s  (682.270s elapsed)
  Total   time  677.414s  (675.450s elapsed)
  

• With --no-infer-absurd-clauses and absurd clauses added manually:

  Total   time  653.221s  (651.480s elapsed)
  Total   time  663.088s  (661.350s elapsed)
  

In this case manual insertion of absurd clauses does not seem to have had much of an effect, except that, in my opinion, the code became uglier. I suggest that we give recommendations for when it might make sense to try turning off inference of absurd clauses:

• One criterion could be that interactive highlighting should indicate that a single definition takes a long time to type-check.
• I wonder if one could be more precise. If interactive highlighting indicates that basically all the time is spent checking right-hand sides, then I guess there is little point in trying to turn off inference of absurd clauses. @oskeri, what information can you glean from interactive highlighting for your code (without the manually inserted absurd clauses)?

Perhaps Agda could even warn if a lot of time is spent on, say, case-splitting.

[oskeri]

@oskeri, what information can you glean from interactive highlighting for your code (without the manually inserted absurd clauses)?

The cases where inserting absurd clauses have had a significant improvement all spent a lot of time on the part of type-checking where the whole definition is highlighted. In the file mentioned above, it spent ~15 s in this state compared to <1 s with the absurd clauses added.