anchor.diff:  
       else match Env.try_lookup_lid env ilid with
            | Some ((_, t), _) ->
  -           check_strictly_positive_argument ty_lid t args
  +           check_strictly_positive_argument env ty_lid t args unfolded
            | None ->
              debug_positivity env (fun () -> "Checking nested positivity, no attrs or type, return false");
              false
  
positive.code:  * This function checks that whereever ty_lid appears in the args,
   *   the corresponding parameter in t is marked strictly positive
   *)
  let check_strictly_positive_argument
    (ty_lid:lident)
    (t:typ)
    (args:args)
    : bool =
    let bs, _ = U.arrow_formals t in
    let rec aux (bs:binders) args : bool =
  
negative.code:          env
           t
           (let must_tot = false in must_tot) in
         check_strictly_positive_argument env ty_lid t_ty args unfolded
       end
       else
         let fv, us = fv_us_opt |> must in
  