anchor.diff:              | Tm_meta (e0, Meta_monadic_lift(m1, m2, t')) -> not (U.is_pure_effect m1)
               | _ -> false
             in
  -          if BU.for_some is_arg_impure ((as_arg head_app)::args) then
  -            Errors.log_issue head.pos
  +          if BU.for_some is_arg_impure ((as_arg head)::args) then
  +            Errors.log_issue top.pos
                                (Errors.Warning_Defensive,
                                 BU.format1 "Incompatibility between typechecker and normalizer; \
                                             this monadic application contains impure terms %s\n"
  -                                          (Print.term_to_string head))
  +                                          (Print.term_to_string top))
           end;
   
           (* GM: I'm really suspicious of this code, I tried to change it the least
            * when trying to fixing it but these two seem super weird. Why 2 of them?
            * Why is it not calling rebuild? I'm gonna keep it for now. *)
           let fallback1 () =
  -            log cfg (fun () -> BU.print2 "Reified (2) <%s> to %s\n" (Print.term_to_string head0) "");
  -            norm cfg env (List.tl stack) (U.mk_reify head)
  +            log cfg (fun () -> BU.print2 "Reified (2) <%s> to %s\n" (Print.term_to_string top0) "");
  +            norm cfg env (List.tl stack) (U.mk_reify top)
           in
           let fallback2 () =
  -            log cfg (fun () -> BU.print2 "Reified (3) <%s> to %s\n" (Print.term_to_string head0) "");
  -            norm cfg env (List.tl stack) (mk (Tm_meta (head, Meta_monadic(m, t))) head0.pos)
  +            log cfg (fun () -> BU.print2 "Reified (3) <%s> to %s\n" (Print.term_to_string top0) "");
  +            norm cfg env (List.tl stack) (mk (Tm_meta (top, Meta_monadic(m, t))) top0.pos)
           in
   
           (* This application case is only interesting for fully-applied dm4f actions. Otherwise,
            * we just continue rebuilding. *)
  -        begin match (U.un_uinst head_app).n with
  +        begin match (U.un_uinst head).n with
           | Tm_fvar fv ->
               let lid = S.lid_of_fv fv in
               let qninfo = Env.lookup_qname cfg.tcenv lid in
  
positive.code:             else
  
              (* Turn it info (reify head) args, then do_unfold_fv will kick in on the head *)
              let t = S.mk_Tm_app (U.mk_reify head_app) args None t.pos in
              norm cfg env (List.tl stack) t
  
          | _ ->
  
negative.code:       (* (should be checked at typechecking and elaborated with an explicit binding if needed) *)
        (* reify (match e with p -> e') ~> match e with p -> reify e' *)
        let branches = branches |> List.map (fun (pat, wopt, tm) -> pat, wopt, U.mk_reify tm) in
        let tm = mk (Tm_match(e, branches)) top.pos in
        norm cfg env (List.tl stack) tm
  
      | _ ->
  