anchor.diff:  let bind r1 env e1opt (lc1:lcomp) ((b, lc2):lcomp_with_binder) : lcomp =
     let lc1 = N.ghost_to_pure_lcomp env lc1 in //downgrade from ghost to pure, if possible
     let lc2 = N.ghost_to_pure_lcomp env lc2 in
  +  let joined_eff = join_lcomp env lc1 lc2 in
     if debug env Options.Extreme
     then
       (let bstr = match b with
  
positive.code: let weaken_precondition env lc (f:guard_formula) : lcomp =
    let weaken () =
        let c = lc.comp () in
        match f with
        | Trivial -> c
        | NonTrivial f ->
          if Util.is_ml_comp c
          then c
          else let c = Normalize.unfold_effect_abbrev env c in
               let u_res_t, res_t, wp = destruct_comp c in
               let md = Env.get_effect_decl env c.effect_name in
               let wp = mk_Tm_app (inst_effect_fun_with [u_res_t] env md md.assume_p)  [S.as_arg res_t; S.as_arg f; S.as_arg wp]  None wp.pos in
               mk_comp md u_res_t res_t wp c.flags in
    {lc with comp=weaken}
  
  let strengthen_precondition (reason:option<(unit -> string)>) env (e:term) (lc:lcomp) (g0:guard_t) : lcomp * guard_t =
  
negative.code:         | NonTrivial f ->
            let g = {g with guard_f=Trivial} in
            let strengthen () =
                if env.lax then
                  lc.comp()
                else begin
                    //try to normalize one more time, since more unification variables may be resolved now
                    let f = N.normalize [N.Beta; N.Eager_unfolding; N.Simplify] env f in
                    match (SS.compress f).n with
                        | Tm_abs(_, {n=Tm_fvar fv}, _) when S.fv_eq_lid fv Const.true_lid ->
                          //it's trivial
                          let lc = {lc with res_typ=t} in
                          lc.comp()
  
                        | _ ->
                            let c = lc.comp() in
                            if Env.debug env <| Options.Extreme
                            then Util.print4 "Weakened from %s to %s\nStrengthening %s with guard %s\n"
                                    (N.term_to_string env lc.res_typ)
                                    (N.term_to_string env t)
                                    (N.comp_to_string env c)
                                    (N.term_to_string env f);
  
                            let ct = Normalize.unfold_effect_abbrev env c in
                            let a, kwp = Env.wp_signature env Const.effect_PURE_lid in
                            let k = SS.subst [NT(a, t)] kwp in
                            let md = Env.get_effect_decl env ct.effect_name in
                            let x = S.new_bv (Some t.pos) t in
                            let xexp = S.bv_to_name x in
                            let u_t, _, _ = destruct_comp ct in
                            let wp = mk_Tm_app (inst_effect_fun_with [u_t] env md md.ret_wp)
                                               [S.as_arg t; S.as_arg xexp]
                                               (Some k.n) xexp.pos
                            in
                            let cret = Util.lcomp_of_comp <| mk_comp md u_t t wp [RETURN] in
                            let guard = if apply_guard
                                        then mk_Tm_app f [S.as_arg xexp] (Some U.ktype0.n) f.pos
                                        else f
                            in
                            let eq_ret, _trivial_so_ok_to_discard =
                                strengthen_precondition (Some <| Errors.subtyping_failed env lc.res_typ t)
                                                        (Env.set_range env e.pos) e cret
                                                        (guard_of_guard_formula <| NonTrivial guard)
                            in
                            let x = {x with sort=lc.res_typ} in
                            let c = bind e.pos env (Some e) (Util.lcomp_of_comp <| mk_Comp ct) (Some x, eq_ret) in
                            let c = c.comp () in
                            if Env.debug env <| Options.Extreme
                            then Util.print1 "Strengthened to %s\n" (Normalize.comp_to_string env c);
                            c
                  end
            in
            let flags = lc.cflags |> List.collect (function
                                                   | RETURN | PARTIAL_RETURN -> [PARTIAL_RETURN]
  