[ pre-release ] compatibility with Agda 2.5.3

src/Data/List/Sized/Interface.agda

@@ -28,6 +28,6 @@ open import Data.Product.N-ary
 instance
 
   sized-nary : ∀ {ℓ} {A : Set ℓ} → Sized A (A ^_)
-  Sized.view sized-nary {0}    xs = Level.lift tt
-  Sized.view sized-nary {1}    x  = x , Level.lift tt
-  Sized.view sized-nary {2+ n} xs = xs
+  Sized.view sized-nary {0}           xs = Level.lift tt
+  Sized.view sized-nary {1}           x  = x , Level.lift tt
+  Sized.view sized-nary {suc (suc n)} xs = xs

src/Text/Parser/Monad.agda

@@ -3,7 +3,7 @@ module Text.Parser.Monad where
 open import Data.Empty
 open import Data.Unit
 open import Data.Char
-open import Data.Product hiding (,_)
+open import Data.Product as Prod hiding (,_)
 open import Data.List hiding (fromMaybe ; [_])
 open import Data.Vec using (Vec)
 open import Data.Maybe hiding (monad ; monadT ; monadZero ; monadPlus)
@@ -96,14 +96,14 @@ module AgdarsecT
   getAnnotations = proj₂ ST.<$> ST.get
 
   withAnnotation : ∀ {A} → C → AgdarsecT E C M A → AgdarsecT E C M A
-  withAnnotation c ma = let open ST in do
-    ST.modify (map₂ (c ∷_))
-    a ← ma
-    ST.modify (map₂ (drop 1))
+  withAnnotation c ma = let open ST in
+    ST.modify (Prod.map id (c ∷_)) >>
+    ma >>= λ a →
+    ST.modify (Prod.map id (drop 1)) >>
     ST.pure a
 
   recordChar : Char → AgdarsecT E C M ⊤
-  recordChar c = tt ST.<$ ST.modify (map₁ (next c))
+  recordChar c = tt ST.<$ ST.modify (Prod.map (next c) id)
 
   -- Commiting to a branch makes all the failures in that branch hard failures
   -- that we cannot recover from