Effects SteelSel and SteelSelF (or PURE and SteelSel(F)) cannot be composed

[R1kM]

This issue often occurs when a program contains different branches, through if/then/else or pattern matching.
For instance,

let test_if (r:ref int) : SteelSel unit
  (vptr r) (fun _ -> vptr r)
  (requires fun _ -> True)
  (ensures fun _ _ _ -> True)
  = if true then (write r 1)
    else (write r 0; write r 0)

We currently do not have polymonadic if/then/elses. Any composite Steel computation will have effect Steel(Sel)F, while function calls will often have effect Steel(Sel)F.

A temporary workaround is to force the if branch into the SteelSelF effect, by adding a noop computation. This can be done by replacing write r 1 by noop (); write r 1