anchor.diff:        (List.map U_name ty_us)
         unfolded_inductives) (snd (datacons_of_typ env ty_lid))
   
  -let name_strictly_positive_in_type env bv t =
  -  let fv_lid = lid_of_str "__fv_lid_for_positivity_checking__" in
  -  let fv = S.tconst fv_lid in
  -  let t = SS.subst [NT (bv, fv)] t in
  -  ty_strictly_positive_in_type env fv_lid t (BU.mk_ref [])
  -
   (* Special-casing the check for exceptions, the single open inductive type we handle. *)
   let check_exn_positivity (env:env_t) (data_ctor_lid:lid) : bool =
     //memo table, memoizes the Tm_app nodes for inductives that we have already unfolded
  
positive.code:      Env.ForExtraction;
       Env.Unascribe;
       Env.AllowUnboundUniverses] env btype in
    debug_positivity env (fun () -> "Checking strict positivity in type, after normalization: " ^ (Print.term_to_string btype));
    not (ty_occurs_in ty_lid btype) ||  //true if ty does not occur in btype
      (debug_positivity env (fun () -> "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
         let fv_us_opt = try_get_fv t in
         if fv_us_opt |> is_none then begin
           debug_positivity env (fun () -> "ty is an app node with head that is not an fv, returning false");
           false  //head is not an fv, ok
         end
         else
           let fv, us = fv_us_opt |> must 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_positivity env (fun () -> "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_positivity env (fun () -> "Checking strict positivity in the Tm_app node, head lid is not ty, so checking nested positivity") in
             ty_nested_positive_in_inductive env ty_lid fv.fv_name.v us args unfolded
  
       | Tm_arrow (sbs, c) ->  //binder type is an arrow type
         debug_positivity env (fun () -> "Checking strict positivity in Tm_arrow");
         let check_comp =
           let c = Env.unfold_effect_abbrev env c |> mk_Comp in
           U.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_positivity env (fun () -> "Checking strict positivity , the arrow is impure, so return true") in
           true
         else
           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 (push_binders env sbs) ty_lid return_type unfolded)
       | Tm_fvar _
       | Tm_uinst _ 
       | Tm_type _ ->
         debug_positivity env (fun () -> "Checking strict positivity in an fvar/Tm_uinst/Tm_type, return true");
         true  //if it's just an fvar, should be fine
       | Tm_refine (bv, _) ->
         debug_positivity env (fun () -> "Checking strict positivity in an Tm_refine, recur in the bv sort)");
         ty_strictly_positive_in_type env ty_lid bv.sort unfolded
       | 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 (push_binders env bs) ty_lid t unfolded 
         ) branches
       | Tm_ascribed (t, _, _) ->
         debug_positivity env (fun () -> "Checking strict positivity in an Tm_ascribed, recur)");
         ty_strictly_positive_in_type env ty_lid t unfolded
       | _ ->
         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
  
  //some binder of some data constructor is an application of ilid to the args
  //ilid may not be an inductive, in which case we simply return false
  
negative.code: | _ -> failwith "Nested positive check, unhandled case"
  
  
  let name_strictly_positive_in_type env bv t =
    let fv_lid = lid_of_str "__fv_lid_for_positivity_checking__" in
    let fv = S.tconst fv_lid in
    let t = SS.subst [NT (bv, fv)] t in
    ty_strictly_positive_in_type env fv_lid t (BU.mk_ref [])
  
  //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
  