anchor.diff:                (* We are in the case where [head] = [bind e (fun x -> return x)] *)
                 (* which can be optimised to just keeping normalizing [e] with a reify on the stack *)
                 norm cfg env stack lb.lbdef
  -            else
  +            else (
                 (* TODO : optimize [bind (bind e1 e2) e3] into [bind e1 (bind e2 e3)] *)
                 (* Rewriting binds in that direction would be better for exception-like monad *)
                 (* since we wouldn't rematch on an already raised exception *)
  +              let rng = head.pos in
  +
                 let head = U.mk_reify <| lb.lbdef in
                 let body = U.mk_reify <| body in
                 (* TODO : Check that there is no sensible cflags to pass in the residual_comp *)
  
positive.code:                 | Tm_uinst (bind, [_ ; _]) ->
                      S.mk (Tm_uinst (bind, [ cfg.tcenv.universe_of cfg.tcenv (close lb.lbtyp)
                                            ; cfg.tcenv.universe_of cfg.tcenv (close t)]))
                      None head.pos
                  | _ -> failwith "NIY : Reification of indexed effects"
                in
                let reified = S.mk (Tm_app(bind_inst, [
  
negative.code:                   as_arg S.tun; as_arg head;
                    (* wp_body, body--the term shouldn't depend on wp_body *)
                    as_arg S.tun; as_arg body]))
                  None rng
                in
                norm cfg env (List.tl stack) reified
              )
        end
      | Tm_app (head_app, args) ->
          (* ****************************************************************************)
  