Fix regressions

examples/tactics/NormLHS.fst

@@ -16,7 +16,7 @@ let norm_lhs steps : Tac unit =
     | _ ->
       fail "not an eq"
 
-type unit_t = unit
+let unit_t = unit
 
 let tau () = norm_lhs [delta; hnf; weak]; trefl ()
 

tests/micro-benchmarks/BinderAttributes.fst

@@ -9,7 +9,7 @@ let default_to (def : 'a) (x : option 'a) : Tot 'a =
     | None -> def
     | Some a -> a
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type inductive_example =
     | CaseExplicit : [@@@ description "x"] x:int -> [@@@ description "y"] y:string -> inductive_example

tests/micro-benchmarks/MultipleAttributesBinder.fst

@@ -7,9 +7,9 @@ type attr_value =
     | String : v:string -> attr_value
     | Int : v:int -> attr_value
 
-type attr1 (v : string) = ()
-type attr2 (v : int) = ()
-type attr3 (v : attr_value) = ()
+let attr1 (v : string) = ()
+let attr2 (v : int) = ()
+let attr3 (v : attr_value) = ()
 
 let f (#[@@@ attr1 "imp"; attr2 1; attr3 (String "x")] x_imp:int) ([@@@ attr1 "exp"; attr2 2; attr3 (String "y")] y:string) : Tot unit =
     ()

tests/micro-benchmarks/RecordFieldAttributes.fst

@@ -2,7 +2,7 @@ module RecordFieldAttributes
 
 module T = FStar.Tactics.V2
 
-type description (d : string) = ()
+let description (d : string) = ()
 
 type r = 
     {

ulib/FStar.FiniteMap.Base.fst

@@ -43,7 +43,7 @@ open FStar.FiniteSet.Ambient
 module T = FStar.Tactics.V2
 
 // Finite maps
-type map (a: eqtype) (b: Type u#b) = (keys: FSet.set a) & (setfun_t a b keys)
+type map (a: eqtype) ([@@@ strictly_positive] b: Type u#b) = (keys: FSet.set a) & (setfun_t a b keys)
 
 let domain (#a: eqtype) (#b: Type u#b) (m: map a b) : FSet.set a =
   let (| keys, _ |) = m in 

ulib/FStar.IntegerIntervals.fst

@@ -38,13 +38,13 @@ type interval_type (x y:int) = z : Type0{ z == t:int{interval_condition x y t} }
 type interval (x y: int) : interval_type x y = t:int{interval_condition x y t}
 
 (* general finite integer intervals *)
-type efrom_eto (x y: int) = interval (x+1) y
-type efrom_ito (x y: int) = interval (x+1) (y+1)
-type ifrom_eto (x y: int) = interval x y
-type ifrom_ito (x y: int) = interval x (y+1)
+type efrom_eto (x y: int) : interval_type _ _ = interval (x+1) y
+type efrom_ito (x y: int) : interval_type _ _ = interval (x+1) (y+1)
+type ifrom_eto (x y: int) : interval_type _ _ = interval x y
+type ifrom_ito (x y: int) : interval_type _ _ = interval x (y+1)
 
 (* Special case for naturals under k, to use in sequences, lists, arrays, etc *)
-type under (k: nat) = interval 0 k
+type under (k: nat) : interval_type 0 k = interval 0 k
 
 (* If we define our intervals this way, then the following lemma comes for free: *)
 private let closed_interval_lemma (x y:int) : Lemma (interval x (y+1) == ifrom_ito x y) = ()
@@ -55,7 +55,7 @@ let interval_size (#x #y: int) (interval: interval_type x y) : nat
   = if y >= x then y-x else 0
 
 (* when we want a zero-based index that runs over an interval, we use this *)
-type counter_for (#x #y:int) (interval: interval_type x y) = under (interval_size interval)
+type counter_for (#x #y:int) (interval: interval_type x y) : Type = under (interval_size interval)
 
 (* special case for closed intervals, used in FStar.Algebra.CommMonoid.Fold *)
 let closed_interval_size (x y: int) : nat = interval_size (ifrom_ito x y)

ulib/FStar.PartialMap.fst

@@ -20,13 +20,13 @@ module FStar.PartialMap
 
 open FStar.FunctionalExtensionality
 
-type t k v = k ^-> option v
+type t (k:eqtype) ([@@@strictly_positive] v:Type u#a) = k ^-> option v
 
 let empty _ _ = on_dom _ (fun _ -> None)
 let literal f = on_dom _ (fun x -> f x)
 let sel m x = m x
-let upd m x y = on_dom _ (fun x1 -> if x1 = x then Some y else m x1)
-let remove m x = on_dom _ (fun x1 -> if x1 = x then None else m x1)
+let upd (#k:eqtype) #v m x y = on_dom _ (fun (x1:k) -> if x1 = x then Some y else m x1)
+let remove (#k:eqtype) m x = on_dom _ (fun (x1:k) -> if x1 = x then None else m x1)
 
 let sel_empty _ _ = ()
 let sel_literal _ _ = ()

ulib/experimental/FStar.OrdSet.fst

@@ -15,7 +15,7 @@
 *)
 module FStar.OrdSet
 
-type ordset a f = l:(list a){sorted f l}
+type ordset (a:eqtype) f = l:(list a){sorted f l}
 
 let hasEq_ordset _ _ = ()
 

ulib/experimental/FStar.Sequence.Base.fst

@@ -44,7 +44,7 @@ module FLT = FStar.List.Tot
 
 /// Internally, we represent a sequence as a list.
 
-type seq (ty: Type) = list ty
+type seq ([@@@ strictly_positive] ty: Type u#a) = list ty
 
 /// We represent the Dafny function `Seq#Length` with `length`:
 ///