anchor.diff:                                                    S.range_of_bv hd))
                       | _ -> ()
                  end;
  +               (* since binders depend on previous ones, we accumulate a substitution *)
                  let expected_t = SS.subst subst hd_expected.sort in
                  let t, g = match (U.unmeta hd.sort).n with
                       | Tm_unknown -> expected_t, g
  +                    (* in case we have an annotation on both implementation and declaration, we:
  +                      * 1) type check the implementation type
  +                      * 2) add an extra guard that the two types must be equal (use_eq will be used in Rel.teq
  +                    *)
                       | _ ->
                         if Env.debug env Options.High then BU.print1 "Checking binder %s\n" (Print.bv_to_string hd);
                         let t, _, g1 = tc_tot_or_gtot_term env hd.sort in
  
positive.code:                 (Rel.guard_to_string env g) (Rel.guard_to_string env guard);
       let msg = if Rel.is_trivial g then None else (Some <| Err.subtyping_failed env t t') in
       let g = Rel.conj_guard g guard in
       let lc, g = TcUtil.strengthen_precondition msg env e lc g in
       memo_tk e t', set_lcomp_result lc t', g in
    if debug env Options.Low
  
negative.code:     e, S.mk_Total t |> U.lcomp_of_comp, (Rel.conj_guard g0 g1)
  
    | Tm_name x ->
      let t, rng =
          if env.use_bv_sorts
          then x.sort, S.range_of_bv x
          else Env.lookup_bv env x in
      let x = S.set_range_of_bv ({x with sort=t}) rng in
      FStar.TypeChecker.Common.insert_bv x t;
  