This problem is a little convoluted to describe in a generic fashion, I'm just leaving the specific example for later investigation.
Consider the following stencil:
neighbors(C2Eₒ, (↑(λ(__arg0) → cast_(·__arg0, float64)))(⟪Koffₒ, -1ₒ⟫(__stencil_arg2))))
This stencil is only valid when when __stencil_arg2 can be derefed with a Koff of -1. However now consider we unroll the neighbor reduction we become
λ(_acc_10, _i_11) → if can_deref(⟪Koffₒ, -1ₒ, C2CEₒ, _i_11⟫(__stencil_arg1))
then _acc_10 + ·⟪Koffₒ, -1ₒ, C2CEₒ, _i_11⟫(__stencil_arg1)
× cast_(·⟪Koffₒ, -1ₒ, C2Eₒ, _i_11⟫(__stencil_arg2), float64)
else _acc_10
Now suddenly this is unconditionally valid as can_deref will just mask the previously invalid accesses in K.