anchor.diff:      in
       norm cfg env (Meta(metadata, head.pos)::stack) head
   
  -and do_reify_monadic cfg env stack (head : term) (m : monad_name) (t : typ) : term=
  +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));
       match (SS.compress head).n with
       | Tm_let ((false, [lb]), body) ->
         (* ****************************************************************************)
  
positive.code:               else tail in
              norm cfg' env stack' tm
  
            | Tm_app({n=Tm_constant Const_range_of}, a1::a2::rest)
            | Tm_app({n=Tm_constant FC.Const_reify}, a1::a2::rest) ->
              let hd, _ = U.head_and_args t in
              let t' = S.mk (Tm_app(hd, [a1])) None t.pos in
              let t = S.mk(Tm_app(t', a2::rest)) None t.pos in
              norm cfg env stack t
  
            | Tm_app({n=Tm_constant Const_set_range_of}, a1::a2::a3::rest) ->
              let hd, _ = U.head_and_args t in
              let t' = S.mk (Tm_app(hd, [a1;a2])) None t.pos in
              let t = S.mk(Tm_app(t', a3::rest)) None t.pos in
              norm cfg env stack t
  
            | Tm_app({n=Tm_constant (FC.Const_reflect _)}, [a])
                  when (cfg.steps |> List.contains Reify &&
                        is_reify_head stack) ->
              norm cfg env (List.tl stack) (fst a)
  
            | Tm_app({n=Tm_constant FC.Const_reify}, [a])
                  when (cfg.steps |> List.contains Reify) ->
              let reify_head, _ = U.head_and_args t in
              let a = SS.compress (U.unascribe <| fst a) in
              //BU.print2_warning "TRYING NORMALIZATION OF REIFY: %s ... %s\n" (Print.tag_of_term a) (Print.term_to_string a);
              begin match a.n with
                (* KM : This assumes that reflect is never tagged by a Meta_monadic flag *)
                (* Is that really the case ? *)
                | Tm_app({n=Tm_constant (FC.Const_reflect _)}, [a]) ->
                  //reify (reflect e) ~> e
                  norm cfg env stack (fst a)
  
                (* KM : This case reall y does not make any sense to me *)
                // | Tm_match(e, branches) ->
                //   //reify (match e with p -> e') ~> match (reify e) with p -> reify e'
                //   let e = U.mk_reify e in
                //   let branches = branches |> List.map (fun (pat, wopt, tm) -> pat, wopt, U.mk_reify tm) in
                //   let tm = mk (Tm_match(e, branches)) t.pos in
                //   norm cfg env stack tm
  
                | _ ->
                  let stack = App(env, reify_head, None, t.pos)::stack in
                  norm cfg env stack a
              end
  
            | Tm_type u ->
              let u = norm_universe cfg env u in
              rebuild cfg env stack (mk (Tm_type u) t.pos)
  
negative.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..)
      | Tm_meta(e, Meta_monadic _) ->
          do_reify_monadic fallback cfg env stack e m t
  
      | Tm_meta(e, Meta_monadic_lift (msrc, mtgt, t')) ->
          let lifted = reify_lift cfg e msrc mtgt (closure_as_term cfg env t') in
          norm cfg env (List.tl stack) lifted
  
      | Tm_match(e, branches) ->
        (* Commutation of reify with match, note that the scrutinee should never be effectful    *)
        (* (should be checked at typechecking and elaborated with an explicit binding if needed) *)
  