anchor.diff:                    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 head.pos
  +                None rng
                 in
                 norm cfg env (List.tl stack) reified
  +            )
         end
       | Tm_app (head_app, args) ->
           (* ****************************************************************************)
  
positive.code:               (* 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
                (* 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 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 *)
  
negative.code:     in
      norm cfg env (Meta(metadata, head.pos)::stack) head
  
  and do_reify_monadic fallback cfg env stack (head : term) (m : monad_name) (t : typ) : term =
      (* Precondition: the stack head is an App (reify, ...) *)
      let head = U.unascribe head in
      log cfg (fun () -> BU.print2 "Reifying: (%s) %s\n" (Print.tag_of_term head) (Print.term_to_string head));
  