make mkRawMonad and mkRawApplicative universe-polymorphic (#2314)

* make `mkRawMonad` and `mkRawApplicative` universe-polymorphic

* fix unresolved metas

---------

Co-authored-by: Gan Shen <[email protected]>

Author: 2 people

src/Data/Product/Effectful/Left.agda

@@ -49,7 +49,7 @@ monad = record
   }
 
 -- The monad instance also requires some mucking about with universe levels.
-monadT : RawMonadT (_∘′ Productₗ)
+monadT : ∀ {ℓ} → RawMonadT {g₁ = ℓ} (_∘′ Productₗ)
 monadT M = record
   { lift = (ε ,_) <$>_
   ; rawMonad = mkRawMonad _

src/Data/Product/Effectful/Right.agda

@@ -48,7 +48,7 @@ monad = record
   ; _>>=_ = uncurry λ a w₁ f → map₂ (w₁ ∙_) (f a)
   }
 
-monadT : RawMonadT (_∘′ Productᵣ)
+monadT : ∀ {ℓ} → RawMonadT {g₁ = ℓ} (_∘′ Productᵣ)
 monadT M = record
   { lift = (_, ε) <$>_
   ; rawMonad = mkRawMonad _

src/Effect/Applicative.agda

@@ -77,7 +77,7 @@ module _ where
 
   -- Smart constructor
   mkRawApplicative :
-    (F : Set f → Set f) →
+    (F : Set f → Set g) →
     (pure : ∀ {A} → A → F A) →
     (app : ∀ {A B} → F (A → B) → F A → F B) →
     RawApplicative F

src/Effect/Monad.agda

@@ -74,7 +74,7 @@ module _ where
   open RawApplicative
 
   mkRawMonad :
-    (F : Set f → Set f) →
+    (F : Set f → Set g) →
     (pure : ∀ {A} → A → F A) →
     (bind : ∀ {A B} → F A → (A → F B) → F B) →
     RawMonad F

src/Reflection/AST/DeBruijn.agda

@@ -116,7 +116,7 @@ module _ where
 module _ where
 
   private
-    anyApplicative : RawApplicative (λ _ → Bool)
+    anyApplicative : ∀ {ℓ} → RawApplicative {ℓ} (λ _ → Bool)
     anyApplicative = mkRawApplicative _ (λ _ → false)  _∨_
 
   open Traverse anyApplicative