This example would work fine with non-GADT syntax, right? That is

{-@ MkId :: Prop (Term id) @-}
data Term = MkId

This solution can be broken in four steps.

First, extract equalities from bindings that are about the same terms. e.g.

{v:_ | prop v = Term id && someOtherPredicate v }
{v:_ | prop v = Term f}
{k:_ | k = Term g && k = Term h}

would produce equalities

prop v = Term id
prop v = Term f
k = Term g
k = Term h

Second, infer equalities of data constructors by transitivity.

Term id = Term f
Term g = Term h

Third, infer rewrites on the arguments of data constructors, obtaining

id ~> f
f ~> id
g ~> h
h ~> g

Fourth, discard sufficient rewrites to ensure termination of rewriting.

f ~> id
g ~> h

Now f can be replaced with identity whenever found.

The fourth step is so far underspecified. Users of LF need to indicate what variables are ok to appear in lhs and the rhs of the final rewrites (hence the attempt to decide this based on whether variables are local or global).

We don't generate the unification id ~> f as id is not a "local" and it has a definition

An unknown to this approach: While the criterion to cut loops is not settled, it could happen that LF needs to be more restrictive on what rewrites are accepted, because it has less context on how the rewrites are produced.

If the local rewrites were produced by LH instead, LH could produce more rewrites known to be terminating.

This point arouse when discussing the criterion to use in the fourth step of Solution 2. It could be unsafe to allow local variables in the right-hand side of rewrites, but forbidding local variables there would also discard many innocuous rewrites.

And there is a third approach that is to lean on rest-rewrite to apply the local rewrites, so we don't need to ensure termination separately.

You can add it in the proposal the only thing I'm not sure about is if there is a way to encode lambda into REST terms

We also mentioned that the integration to REST will be much slower because REST is checking for termination, which we do not really need in this case.

I'm just noticing that if the new define form allowed parameters, as the old form does, this mechanism could be reused to unfold local definitions as well.

For instance,

{-@ reflect map @-}
map f e = go
  where
    go [] = e
    go (x:xs) = f x : go xs

{-@ lemma :: f:_ -> e:_ -> { map f e [] == [] } @-}
lemma _ _ = ()

Oh, well, it would have to be spelled out how the binding of go is introduced when doing PLE. So it is not something we could address immediately, but I think it is an interesting derivation of the current effort.

You're right but first we need to allow lambdas in reflected function as GHC is generating lambda when using where clauses to define functions

Edit: I was wrong is another error regarding recursive definitions