anchor.diff:      debug_positivity env (fun () -> "Checking nested positivity in the unfolded data constructor binders as: " ^ (Print.binders_to_string "; " dbs) ^ ", and c: " ^ (Print.comp_to_string c));
       ty_nested_positive_in_type ty_lid (Tm_arrow (dbs, c)) ilid num_ibs unfolded env
     | _ ->
  -    //AR: TODO: 04/21: may be this should be an error since data constructor type is not an arrow?
       debug_positivity 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
   
  
positive.code:          let _ = debug_positivity env (fun () -> "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 ({binder_bv=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_positivity env (fun () -> "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_positivity env (fun () -> "Checking strict positivity in an Tm_type, return true");
         true  //if it's just a Type(u), should be fine
       | Tm_uinst (t, _) ->
         debug_positivity env (fun () -> "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_positivity env (fun () -> "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_positivity env (fun () -> "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_positivity env (fun () -> "Checking strict positivity in an Tm_ascribed, recur)");
         ty_strictly_positive_in_type ty_lid t unfolded env
       | _ ->
         debug_positivity env (fun () -> "Checking strict positivity, unexpected tag: " ^ (Print.tag_of_term btype) ^ " and term: " ^ (Print.term_to_string btype));
         false)  //remaining cases, will handle as they come up
  
negative.code: 
  
  //ty_bs are the opended type parameters of the inductive, and ty_usubst is the universe substitution, again from the ty_lid type
  let ty_positive_in_datacon env (ty_lid:lident) (dlid:lident) (ty_bs:binders) (us:universes) (unfolded:unfolded_memo_t) : bool =
    //get the type of the data constructor
    let dt =
      match Env.try_lookup_and_inst_lid env us dlid with
      | Some (t, _) -> t
      | None -> raise_error (Errors.Error_InductiveTypeNotSatisfyPositivityCondition,
                 BU.format1 "Error looking up data constructor %s when checking positivity"
                   (string_of_lid dlid)) (range_of_lid ty_lid) in
  
    debug_positivity env (fun () -> "Checking data constructor type: " ^ (Print.term_to_string dt));
    
    match (SS.compress dt).n with
    | Tm_fvar _
    | Tm_uinst _ ->
      debug_positivity env (fun () -> "Data constructor type is simply an fvar/Tm_uinst, returning true");
      true  //if the dataconstructor type is simply an fvar, should be an inductive with no params, no indexes, and no binders in data constructor type
  
    | Tm_arrow (dbs, _) ->  //TODO: we should check the computation type is not of the form t (t a), but then typechecker already rejects this type
      //filter out the inductive type parameters, dbs are the remaining binders
      let dbs = snd (List.splitAt (List.length ty_bs) dbs) in
  