[Agda] Type-checker evaluator performance

[effectfully]

I've encountered problems with functions like `Pr' (which is just
`from-just' from the standard library) several times. E.g. using

From-Maybe : ∀ {α β} {A : Set α} -> (A -> Set β) -> Maybe A -> Set β
From-Maybe B  nothing = Lift ⊤
From-Maybe B (just x) = B x

from-Maybe : ∀ {α β} {A : Set α} {B : A -> Set β} -> (∀ x -> B x) ->
(x : Maybe A) -> From-Maybe B x
from-Maybe f  nothing = _
from-Maybe f (just x) = f x

`from-Maybe proj₂ x` consumed three times more memory than `proj₂
(from-just x)` and was noticeably slower.

I don't know whether this is the same case, but have you tried to
normalize `petersons-search' by C-c C-n?