Effect actions cannot be universe polymorphic

[TheoWinterhalter]

It seems that defining actions directly in an effect or layered_effect results in an error message. Below is an example which works:

module MWE

let wpost a = a -> Type0

let wp a = wpost a -> Type0

let theta #a (x : a) : wp a =
  fun post -> post x

let repr a (w : wp a) =
  x : a { forall (post : wpost a). w post ==> theta x post }

let wret #a (x : a) : wp a =
  fun post -> post x

let wbind #a #b (w : wp a) (wf : (x:a) -> wp b) : wp b =
  fun post -> w (fun x -> wf x post)

let return a (x : a) : repr a (wret x) =
  x

let bind a b w wf (m : repr a w) (f : (x:a) -> repr b (wf x)) : repr b (wbind w wf) =
  f m

assume val wact : a:Type -> wp a -> wp a
assume val act : a:Type0 -> w : wp a -> repr a w -> repr a (wact a w)

[@@allow_informative_binders]
reifiable total layered_effect {
  FOO : a:Type -> w: wp a -> Effect
  with
    repr         = repr ;
    return       = return ;
    bind         = bind ;
    act          = act
}

But by replacing Type0 with Type we obtain the following error message:

(Error 200) Expected and generalized universes in the declaration for MWE.FOO:MWE.__proj__FOO__item__act are different, input: , but after gen: uu__4249

@aseemr worked out the following example using effect:

module Test

type unit : Type = unit

type repr (a:Type) (_:unit) = int -> a & int

assume val return (a:Type) (x:a) : repr a ()
assume val bind (a:Type) (b:Type) (f:repr a ()) (g:a -> repr b ()) : repr b ()

assume val act (b:Type) (y:b) : repr int ()

effect {
  MST (a:Type) (_:unit)
  with { repr; return; bind; act =  act }
}