anchor.diff:            | Tm_meta (head, m) ->
               begin match m with
                 | Meta_monadic (m, t) ->
  -                log cfg (fun () -> BU.print2 "Will %sreify : %s \n"
  -                                             (if should_reify cfg stack then "" else "not ")
  -                                             (stack_to_string stack));
  -                if should_reify cfg stack
  -                then do_reify_monadic cfg env stack head m t
  -                else reduce_impure_comp cfg env stack head (Inl m) t
  +                reduce_impure_comp cfg env stack head (Inl m) t
   
                 | Meta_monadic_lift (m, m', t) ->
  -                if should_reify cfg stack
  -                then
  -                    norm cfg env (List.tl stack) (reify_lift cfg.tcenv head m m' (closure_as_term cfg env t))
  -                else reduce_impure_comp cfg env stack head (Inr (m, m')) t
  +                reduce_impure_comp cfg env stack head (Inr (m, m')) t
   
                 | _ ->
                   if List.contains Unmeta cfg.steps
  
positive.code:       | Some (_, a) ->
          let t = S.extend_app t (a,aq) None r in
          rebuild cfg env_arg stack t
      end
  
    | App(env, head, aq, r)::stack ->
  
negative.code:     norm cfg env (Meta(metadata, t.pos)::stack) head
  
  and do_reify_monadic cfg env stack (head : term) (m : monad_name) (t : typ) : term=
      (* Precondition: the stack head is an App (reify, ...) *)
      match (SS.compress head).n with
      | Tm_let ((false, [lb]), body) ->
        (* ****************************************************************************)
  