anchor.diff:  
   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 head0 = head in
       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));
       match (SS.compress head).n with
  
positive.code:           (* An action was found and successfully unfolded *)
            | Some true -> body
          in
          norm cfg env (List.tl stack) body
  
      // Doubly-annotated effect.. just take the outmost one. (unsure..)
  
negative.code:         let mk tm = S.mk tm None head.pos in
          let body = mk (Tm_app(head_app, args)) in
          let body = match found_action with
            (* This is not an action let's just keep the reify marker *)
            | None -> U.mk_reify body
  
            (* The action was found but not unfolded (maybe abstract ?) *)
  