Rewrite "obvious" non-terminating expressions

This is more so an inquiry than an issue or feature request about rewriting "non-terminating" expressions that are possible to be rewritten at compile time to be terminating.

Specifically I was thinking of expressions like filter even (repeat 3) which "are" [] but never manage to evaluate this and instead end up in an infinite loop. A simple rewrite rule forall f x. filter f (repeat x) = if f x then repeat x else [] would allow for the expression mentioned above to evaluate to [] without changing semantics.

There are a lot more examples like forall f x. all f (repeat x) = f x or forall x. or (repeat x) = x and the list goes on.

I doubt this would have much / any use in code as these are so overly specific and wouldn't be in any sensible codebase. I still wanted to bring this up to see whether there is any way to rewrite expressions like this that would be beneficial to the compiler or base.

Another pitfall is that compiling with optimizations could make code that previously worked not work because of expressions inlining.