Enhance cast worker/wrapper for INLINABLE
In #19890 (closed) we realised that cast worker/wrapper didn't really work properly for functions with an INLINABLE pragma, and hence a stable unfolding. This patch fixes the problem.
Instead of disabling cast w/w when there is a stable unfolding (as we did before), we now tranfer the stable unfolding to the worker.
It turned out that it was easier to do that if I moved the cast
w/w stuff from prepareBinding
to completeBind
.
Another merit of doing it in completeBind
is this. If we have
f = /\a. e |> co
then in HEAD today prepareBinding
turns this into
f = /\a. let v = e in v |> co
and then simplLazyBind
laboriously floats out the let
to give
v2 = /\a. e
f = /\a. v2 a |> co
Then mkLam
floats the coercion out to give
v2 = /\a. e
f = (/\a. v2 a) |> (forall a. co)
and now I think the next round of simplification may do another cast worker/wrapper.
This is bonkers. Doing cast w/w in completeBind
finesses all of this.