anchor.diff:                          List.mapi (fun i ((pi, _), (ei, _)) ->
                               let projector = Env.lookup_projector env f.v i in
                               //NS: TODO ... should this be a marked as a record projector? But it doesn't matter for extraction
  -                            match Env.try_lookup_lid env projector with
  -                            | None ->
  -                              failwith (BU.format1 "Impossible: projector %s not found" (Print.lid_to_string projector))
  -                            | _ ->
  -                              let proj = S.fvar (Ident.set_lid_range projector f.p) (Delta_equational_at_level 1) None in
  -                              let sub_term = mk_Tm_app proj [as_arg scrutinee_tm] None f.p in
  -                              build_branch_guard sub_term pi ei) |>
  +                            let scrutinee_tm =
  +                                match Env.try_lookup_lid env projector with
  +                                | None ->
  +                                  None //no projector, e.g., because we are actually typechecking the projector itself
  +                                | _ ->
  +                                  let proj = S.fvar (Ident.set_lid_range projector f.p) (Delta_equational_at_level 1) None in
  +                                  Some (mk_Tm_app proj [as_arg (force_scrutinee())] None f.p)
  +                            in
  +                            build_branch_guard scrutinee_tm pi ei) |>
                           List.flatten
                        in
  -                     discriminate scrutinee_tm f @ sub_term_guards
  +                     discriminate (force_scrutinee()) f @ sub_term_guards
   
               | Pat_dot_term _, _ -> []
                 //a non-pattern sub-term computed via unification; no guard needeed since it is from a dot pattern
  
positive.code:                 let f = head_constructor pat_exp in
                  if not (Env.is_datacon env f.v)
                  then failwith "Impossible: nullary patterns must be data constructors"
                  else discriminate scrutinee_tm (head_constructor pat_exp)
  
              | Pat_cons (_, pat_args), Tm_app(head, args) ->
                  //application pattern
  
negative.code:               [] //no guard for the unit pattern; it's a singleton
  
              | Pat_constant _c, Tm_constant c ->
  
                [U.mk_eq2 U_zero (tc_constant env pat_exp.pos c) (force_scrutinee()) pat_exp]
  
              | Pat_constant (FStar.Const.Const_int(_, Some _)), _ ->
                //machine integer pattern, cf. #1572
                let _, t, _ = env.type_of env pat_exp in
                [U.mk_eq2 U_zero t (force_scrutinee()) pat_exp]
  
              | Pat_cons (_, []), Tm_uinst _
              | Pat_cons (_, []), Tm_fvar _ ->
  