Add mkey to pts_to instead.

Author: gebner

lib/pulse/lib/Pulse.Lib.Reference.fsti

@@ -31,8 +31,8 @@ val null #a : ref a
 
 val is_null #a (r : ref a) : b:bool{b <==> r == null #a}
 
-val pts_to_uninit (#a: Type u#a) ([@@@mkey]r: ref a) : slprop
-val pts_to (#a:Type u#a) ([@@@mkey]r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a) : slprop
+val pts_to_uninit (#[@@@mkey]a: Type u#a) ([@@@mkey]r: ref a) : slprop
+val pts_to (#[@@@mkey]a:Type u#a) ([@@@mkey]r:ref a) (#[T.exact (`1.0R)] p:perm) (n:a) : slprop
 
 instance val is_send_pts_to #a r #p n : is_send (pts_to #a r #p n)
 instance val is_send_pts_to_uninit #a r : is_send (pts_to_uninit #a r)

src/checker/Pulse.Checker.Prover.fst

@@ -754,10 +754,7 @@ let is_mkey (t:R.term) : bool =
   | _ -> false
 
 let binder_is_mkey (b:R.binder) : bool =
-  if List.Tot.existsb is_mkey (R.inspect_binder b).attrs then true else
-  // Treat type arguments as mkeys, as F* will happily unify terms of different types.
-  if R.Tv_Type? (R.inspect_ln (R.inspect_binder b).sort) then true else
-  false
+  List.Tot.existsb is_mkey (R.inspect_binder b).attrs
 
 let binder_is_pred (b:R.binder) : option nat =
   let doms, c = R.collect_arr_ln (R.inspect_binder b).sort in