idris-lang/Idris-dev — pull request #960 by david-christiansen (2014-03-07 13:48:26+00:00)
Title: Skip unnecessary coverage checking

If the last clause in a definition contains only _, we don't need to
coverage check it. This vastly, vastly improves the speed of this defn:

fourTupleElems : TT -> Maybe (TT, (TT, (TT, TT)))
fourTupleElems (App (App (App (App p ty1) ty2) tm1)
(App (App (App (App p ty3) ty4) tm2)
(App (App (App (App p ty1) ty2) tm3) tm4))) = Just (tm1, tm2, tm3, tm4)
fourTupleElems _ = Nothing

The check is perhaps overly conservative, but that can be improved in the future. Right now, it makes the kinds of deep patterns used in reflection programming much more convenient.