[ perf ] type-level evalutaion of `Prelude.elem` is slow compared to the naïve implementation

[CodingCellist]

This came up as part of a thing I'm currently working on. Due to Prelude.elem being implemented for all Foldables, it is significantly slower at compile-time compared to the "trivial" implementation by hand. The full call chain for Prelude.elem is:

elem   = elemBy (==)   = any   = foldMap   = __bind_foldMap

Which I understand is necessary because we are generalising over all Foldable instances, but it is a shame that it results in the worse performance detailed below.

Steps to Reproduce

Consider the following two modules:

PreludeElem.idr

module PreludeElem

import Data.So
import Data.List

%default total

public export
0 Has42 : So (elem 42 [1..300])
Has42 = Oh

ListElem.idr

module ListElem

import Data.So
import Data.List

%default total

public export
elem' : Eq a => a -> List a -> Bool
elem' _ []        = False
elem' e (x :: xs) = (e == x) || elem' e xs

public export
0 Has42 : So (elem' 42 [1..300])
Has42 = Oh

With each module in its own file, measure the time it takes to type-check each file, for example via:

/usr/bin/time -- idris2 --check path/to/file.idr

Expected Behaviour

The two files should type-check in roughly the same time.

Observed Behaviour

The file using Prelude.elem type-checks in ~1.45 seconds, whereas the file using elem' type-checks in ~0.90 seconds. And this difference gets worse with more complex data types and longer lists (the above is a minimised example).

Thoughts

I don't know if there is much to be done about this, but I thought it was worth raising. Edwin mentioned something about __bind_foldMap being expanded or optimised at run-time, so maybe there is a similar hack we can employ at the type-level?

If nothing can be done, feel free to close this issue : )