Currently, the only way to feed equations to PLE is by reflecting functions.

This is a constraint that prevents entering equations from functions in dependencies unless these functions are reflected, which in turn requires to fork the dependencies to introduce the Liquid Haskell annotations that would have the functions reflected.

I would like a mechanism for assumptions to be introduced to PLE without changing dependencies, and I see three ways forward.

Impostor reflection

Let's say we would like to reflect Prelude.filter from base. Define a function

{-@ reflect myfilter @-}
myfilter p [] = []
myfilter p (x:xs) = if p x then x : myfilter p xs else myfilter p xs

Then tell somehow to LH to use the equations of myfilter every time it finds a call to Prelude.filter.

REST route

Introduce the assumed equations via REST rewrite rules. In this case we need to consider whether we can optimize REST so it is a practical substitute for regular PLE equations.

Type-scanning

Suppose we give the following specification to filter.

assume filter
  :: p:(a -> Bool)
  -> xs:[a]
  -> { v:[a] | v = if null xs then [] else if p (head xs) then head xs : filter p (tail xs) else filter p (tail xs) }

The type reveals how to unfold filter, but PLE is not looking for equations in the predicates of refinement types.
I'm guessing it wouldn't be difficult to have Liquid Haskell or Liquid Fixpoint to produce equations for PLE from this.

Moreover, it can be generalized one day, so PLE can do a bit more than unfolding eventually. e.g. given a definition like

gcd :: {x:Int | x>=0 } -> {y:Int | y>=0} -> { v:Int | mod x v = 0 && mod y v = 0 }
gcd x y = if x < y then gcd (y - x) x else if x > y then gcd y x else x

If PLE encounters gcd a b in a formula, it could add to the environment the fact that mod a (gcd a b) = 0 && mod b (gcd a b) = 0 before continuing with the unfolding of other terms.

I like impostor reflection the most because it saves the most typing. First, it gives the power of Haskell syntax to express the equations. And second, if filter depended on other functions, we could rely on LH to introduce the necessary uninterpreted symbols automatically.

type-scanning is interesting because it can generalize a bit what PLE does, but it does not offer as good an experience as impostor reflection for this use case.

REST route has the advantage to not require any new features. But we still need to mature the implementation, and similarly to type-scanning it offers not as good experience as impostor reflection.