anchor.diff:      let dbs = SS.subst_binders subst dbs in
       let c = SS.subst_comp (SS.shift_subst (List.length dbs) subst) c in
   
  -    debug_log env ("Checking nested positivity in the unfolded data constructor binders as: " ^ (PP.binders_to_string "; " dbs) ^ ", and c: " ^ (PP.comp_to_string c));
  +    debug_log env (fun () -> "Checking nested positivity in the unfolded data constructor binders as: " ^ (PP.binders_to_string "; " dbs) ^ ", and c: " ^ (PP.comp_to_string c));
       ty_nested_positive_in_type ty_lid (Tm_arrow (dbs, c)) ilid num_ibs unfolded env
     | _ ->
  -    debug_log env ("Checking nested positivity in the data constructor type that is not an arrow");
  +    debug_log env (fun () -> "Checking nested positivity in the data constructor type that is not an arrow");
       ty_nested_positive_in_type ty_lid (SS.compress dt).n ilid num_ibs unfolded env  //in this case, we don't have anything to substitute, simply check
   
   //t is some data constructor type of ilid, after ilid type parameters have been substituted
  
positive.code: 
  //check if ty_lid occurs strictly positively in some binder type btype
  let rec ty_strictly_positive_in_type (ty_lid:lident) (btype:term) (unfolded:unfolded_memo_t) (env:env_t) :bool =
    debug_log env ("Checking strict positivity in type: " ^ (PP.term_to_string btype));
    //normalize the type to unfold any type abbreviations, TODO: what steps?
    let btype = N.normalize [Env.Beta; Env.Eager_unfolding; Env.UnfoldUntil delta_constant; Env.Iota; Env.Zeta; Env.AllowUnboundUniverses] env btype in
    debug_log env ("Checking strict positivity in type, after normalization: " ^ (PP.term_to_string btype));
    not (ty_occurs_in ty_lid btype) ||  //true if ty does not occur in btype
      (debug_log env ("ty does occur in this type, pressing ahead");
       match (SS.compress btype).n with
       | Tm_app (t, args) ->  //the binder type is an application
         //get the head node fv, try_get_fv would fail if it's not an fv
         let fv, us = try_get_fv t in
         //if it's same as ty_lid, then check that ty_lid does not occur in the arguments
         if Ident.lid_equals fv.fv_name.v ty_lid then
           let _ = debug_log env ("Checking strict positivity in the Tm_app node where head lid is ty itself, checking that ty does not occur in the arguments") in
           List.for_all (fun (t, _) -> not (ty_occurs_in ty_lid t)) args
           //else it must be another inductive type, and we would check nested positivity, ty_nested_positive fails if fv is not another inductive
           //that case could arise when, for example, it's a type constructor that we could not unfold in normalization
         else
           let _ = debug_log env ("Checking strict positivity in the Tm_app node, head lid is not ty, so checking nested positivity") in
           ty_nested_positive_in_inductive ty_lid fv.fv_name.v us args unfolded env
       | Tm_arrow (sbs, c) ->  //binder type is an arrow type
         debug_log env ("Checking strict positivity in Tm_arrow");
         let check_comp =
           let c = Env.unfold_effect_abbrev env c |> mk_Comp in
           is_pure_or_ghost_comp c || (Env.lookup_effect_quals env (U.comp_effect_name c) |> List.existsb (fun q -> q = S.TotalEffect))
         in
         if not check_comp then
           let _ = debug_log env ("Checking strict positivity , the arrow is impure, so return true") in
           true
         else
           let _ = debug_log env ("Checking struict positivity, Pure arrow, checking that ty does not occur in the binders, and that it is strictly positive in the return type") in
           List.for_all (fun (b, _) -> not (ty_occurs_in ty_lid b.sort)) sbs &&  //ty must not occur on the left of any arrow
             (let _, return_type = SS.open_term sbs (FStar.Syntax.Util.comp_result c) in  //and it must occur strictly positive in the result type
              ty_strictly_positive_in_type ty_lid return_type unfolded (push_binders env sbs)) //TODO: do we need to compress c, if so how?
       | Tm_fvar _ ->
         debug_log env ("Checking strict positivity in an fvar, return true");
         true  //if it's just an fvar, should be fine
       | Tm_type _ ->  //TODO: actually we should not even reach here, it should already be covered by ty_occurs_in check at the beginning
         debug_log env ("Checking strict positivity in an Tm_type, return true");
         true  //if it's just a Type(u), should be fine
       | Tm_uinst (t, _) ->
         debug_log env ("Checking strict positivity in an Tm_uinst, recur on the term inside (mostly it should be the same inductive)");
         ty_strictly_positive_in_type ty_lid t unfolded env
       | Tm_refine (bv, _) ->
         debug_log env ("Checking strict positivity in an Tm_refine, recur in the bv sort)");
         ty_strictly_positive_in_type ty_lid bv.sort unfolded env
       | Tm_match (_, branches) ->
         debug_log env ("Checking strict positivity in an Tm_match, recur in the branches)");
         List.for_all (fun (p, _, t) ->
           let bs = List.map mk_binder (pat_bvs p) in
           let bs, t = SS.open_term bs t in
           ty_strictly_positive_in_type ty_lid t unfolded (push_binders env bs)
         ) branches
       | Tm_ascribed (t, _, _) ->
         debug_log env ("Checking strict positivity in an Tm_ascribed, recur)");
         ty_strictly_positive_in_type ty_lid t unfolded env
       | _ ->
         debug_log env ("Checking strict positivity, unexpected tag: " ^ (PP.tag_of_term btype) ^ " and term: " ^ (PP.term_to_string btype));
         false)  //remaining cases, will handle as they come up
  
  //some binder of some data constructor is an application of ilid to the args
  
negative.code:     in
      b
    | Tm_app (_, _) ->
      debug_log env (fun () -> "Data constructor type is a Tm_app, so returning true");
      true  //if the data constructor type is a simple app, it must be t ..., and we already don't allow t (t ..), so nothing to check here
    | Tm_uinst (t, univs) ->
      debug_log env (fun () -> "Data constructor type is a Tm_uinst, so recursing in the base type");
      ty_strictly_positive_in_type ty_lid t unfolded env
    | _ -> failwith "Unexpected data constructor type when checking positivity"
  
  