Skip to content

Do Cast (and strictness?) WW for functions with stable unfoldings

Simon writes in !3318 (comment 274873):

We could try to transfer the [stable] unfolding to the worker. Maybe that would be better. Example:

f = <big> |> co
 -- f has StableUnfolding <unf>
===>
$wf = <big>
 -- $wf has StableUnfolding (<unf> |> sym co)
f = $wf |> co
 -- f does not have a StableUnfolding

Hmm. Maybe that would be better.

I agree, a stable unfolding doesn't guarantee the binding will inline and in that case we want to inline the wrapper at least.

For the same reason, it might be worthwhile to WW functions with stable unfoldings for strictness.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information