Bump to agda-2.8.0

.github/workflows/ci.yml

@@ -13,11 +13,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
-      - uses: omelkonian/setup-agda@v2.2
+      - uses: omelkonian/setup-agda@v2.3
         with:
-          agda-version: 2.7.0.1
-          stdlib-version: 2.2
-          libraries: agda/agda-stdlib-classes#v2.2
+          agda-version: 2.8.0
+          stdlib-version: 2.3
+          libraries: agda/agda-stdlib-classes#v2.3
           main: standard-library-meta
           deploy: ${{ github.ref == 'refs/heads/master' }}
           token: ${{ secrets.GITHUB_TOKEN }}

Class/MonadError.agda

@@ -1,9 +1,9 @@
 {-# OPTIONS --safe --without-K #-}
 
-open import Level
-
 open import Meta.Prelude
 
+open import Class.Functor
+open import Class.Applicative
 open import Class.Monad
 open import Reflection using (TC; ErrorPart; typeError; catchTC; strErr)
 
@@ -25,16 +25,35 @@ MonadError-TC .catch x h = catchTC x (h [ strErr "TC doesn't provide which error
 ErrorT : (E : Set) → (M : ∀ {f} → Set f → Set f) → ∀ {f} → Set f → Set f
 ErrorT E M A = M (E ⊎ A)
 
-module _ {E : Set} {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ where
+import Data.Sum as Sum
+
+module _ {E : Set} {M : ∀ {a} → Set a → Set a} where
+
+  Functor-ErrorT :  ⦃ _ : Functor M ⦄ → Functor (ErrorT E M)
+  Functor-ErrorT ._<$>_ f = fmap (Sum.map₂ f)
+
+  instance _ =  Functor-ErrorT
 
-  Monad-ErrorT : Monad (ErrorT E M)
+  Applicative-ErrorT : ⦃ _ : Applicative M ⦄ → Applicative (ErrorT E M)
+  Applicative-ErrorT .pure a = pure (inj₂ a)
+  Applicative-ErrorT ._<*>_ f x = _<*>_ {F = M} (fmap go f) x
+    where
+    go : (E ⊎ (A → B)) → (E ⊎ A) → (E ⊎ B)
+    go = λ where
+      (inj₁ e) _ → inj₁ e
+      _ (inj₁ e) → inj₁ e
+      (inj₂ f) (inj₂ a) → inj₂ (f a)
+
+  instance _ =  Applicative-ErrorT
+
+  Monad-ErrorT : ⦃ _ : Monad M ⦄ → Monad (ErrorT E M)
   Monad-ErrorT .return a = return (inj₂ a)
   Monad-ErrorT ._>>=_ x f = x >>= λ where
     (inj₁ e) → return (inj₁ e)
     (inj₂ a) → f a
 
-  MonadError-ErrorT : MonadError E (ErrorT E M)
+  instance _ =  Monad-ErrorT
+
+  MonadError-ErrorT : ⦃ _ : Monad M ⦄ → MonadError E (ErrorT E M)
   MonadError-ErrorT .error e = return (inj₁ e)
-  MonadError-ErrorT .catch x h = x >>= λ where
-    (inj₁ e) → h e
-    (inj₂ a) → return (inj₂ a)
+  MonadError-ErrorT .catch x h = x >>= Sum.[ h , return ]

Class/MonadReader.agda

@@ -4,36 +4,50 @@ module Class.MonadReader where
 
 open import Meta.Prelude
 
-open import Class.Monad
+open import Class.Core
 open import Class.Functor
+open import Class.Applicative
+open import Class.Monad
 open import Class.MonadError
 
 open MonadError ⦃...⦄
 
-record MonadReader (R : Set ℓ) (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Setω where
+record MonadReader (R : Set ℓ) (M : Type↑) ⦃ _ : Monad M ⦄ : Setω where
   field
     ask : M R
     local : ∀ {a} {A : Set a} → (R → R) → M A → M A
 
   reader : ∀ {a} {A : Set a} → (R → A) → M A
   reader f = f <$> ask
-    where instance _ = Functor-M
 
 open MonadReader ⦃...⦄
 
 ReaderT : (R : Set) (M : ∀ {a} → Set a → Set a) → ∀ {a} → Set a → Set a
 ReaderT R M A = R → M A
 
-module _ {R : Set} {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ where
+module _ {R : Set} {M : ∀ {a} → Set a → Set a} where
+
+  Functor-ReaderT : ⦃ Functor M ⦄ → Functor (ReaderT R M)
+  Functor-ReaderT ._<$>_ f ra r = f <$> ra r
+
+  instance _ = Functor-ReaderT
+
+  Applicative-ReaderT : ⦃ Applicative M ⦄ → Applicative (ReaderT R M)
+  Applicative-ReaderT .pure a = const (pure a)
+  Applicative-ReaderT ._<*>_ rf ra r = rf r <*> ra r
+
+  instance _ = Applicative-ReaderT
+
+  Monad-ReaderT : ⦃ Monad M ⦄ → Monad (ReaderT R M)
+  Monad-ReaderT .return a _ = return a
+  Monad-ReaderT ._>>=_ x f r = x r >>= flip f r
 
-  Monad-ReaderT : Monad (ReaderT R M)
-  Monad-ReaderT .return a = λ r → return a
-  Monad-ReaderT ._>>=_ x f = λ r → x r >>= λ a → f a r
+  instance _ = Monad-ReaderT
 
-  MonadReader-ReaderT : MonadReader R (ReaderT R M) ⦃ Monad-ReaderT ⦄
-  MonadReader-ReaderT .ask = λ r → return r
+  MonadReader-ReaderT : ⦃ _ : Monad M ⦄ → MonadReader R (ReaderT R M)
+  MonadReader-ReaderT .ask r = return r
   MonadReader-ReaderT .local f x = x ∘ f
 
   MonadError-ReaderT : ∀ {e} {E : Set e} → ⦃ MonadError E M ⦄ → MonadError E (ReaderT R M)
-  MonadError-ReaderT .error e = λ r → error e
-  MonadError-ReaderT .catch x h = λ r → catch (x r) (λ e → h e r)
+  MonadError-ReaderT .error e _ = error e
+  MonadError-ReaderT .catch x h r = catch (x r) (flip h r)

Class/MonadTC.agda

@@ -90,7 +90,6 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
     runSpeculative   : M (A × Bool) → M A
     getInstances     : Meta → M (List Term)
 
-  instance _ = Functor-M {M = M}
   open MonadError me
 
   runAndReset : M A → M A
@@ -218,7 +217,6 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
 module _ {M : ∀ {f} → Set f → Set f}
   ⦃ m : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mtc : MonadTC M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ where
 
-  instance _ = Functor-M {M = M}
   open MonadError me
   open MonadTC mtc
   open MonadReader mre

Meta/Prelude.agda

@@ -21,7 +21,7 @@ open import Data.Unit public
 open import Data.Sum public
   hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap)
 open import Data.Product public
-  hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith)
+  hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith; _<*>_)
 open import Data.Nat public
   hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_)
 open import Data.String public

Reflection/TCI.agda

@@ -24,13 +24,15 @@ TC : Set ℓ → Set ℓ
 TC = ReaderT TCEnv R.TC
 
 Monad-TC : Monad TC
-Monad-TC = Monad-ReaderT ⦃ Class.Monad.Monad-TC ⦄
+Monad-TC = Monad-ReaderT
 
 MonadReader-TC : MonadReader TCEnv TC ⦃ Monad-TC ⦄
-MonadReader-TC = MonadReader-ReaderT ⦃ Class.Monad.Monad-TC ⦄
+MonadReader-TC = MonadReader-ReaderT
+
+instance _ = Class.MonadError.MonadError-TC
 
 MonadError-TC : MonadError (List ErrorPart) TC
-MonadError-TC = MonadError-ReaderT ⦃ Class.Monad.Monad-TC ⦄ ⦃ Class.MonadError.MonadError-TC ⦄
+MonadError-TC = MonadError-ReaderT
 
 applyReductionOptions : TC A → TC A
 applyReductionOptions x r@record { reduction = onlyReduce red } = R'.withReduceDefs (true ,  red) (x r)

Reflection/Utils/TCI.agda

@@ -21,8 +21,6 @@ open import Class.DecEq
 open import Class.Functor
 open import Class.Traversable
 
-instance _ = Functor-M
-
 fresh-level : M Level
 fresh-level = newMeta (quote Level ∙) >>= unquoteTC
 

Tactic/ClauseBuilder.agda

@@ -93,8 +93,6 @@ singlePatternFromPattern (arg i p) =
 
 module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where
 
-  instance _ = Functor-M {M = M}
-
   ctxSinglePatterns : M (List SinglePattern)
   ctxSinglePatterns = do
     ctx ← getContext
@@ -192,17 +190,14 @@ record ContextMonad (M : ∀ {a} → Set a → Set a) ⦃ _ : Monad M ⦄ : Set
 
 open ContextMonad ⦃...⦄
 
-Monad-Id : Monad id
-Monad-Id .return = id
-Monad-Id ._>>=_  = flip _$_
-
 -- No context
-ContextMonad-Id : ContextMonad id ⦃ Monad-Id ⦄
-ContextMonad-Id .introPatternM _ a = a
+module _ where
+  open import Class.Monad.Id
 
-module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where
+  ContextMonad-Id : ContextMonad id
+  ContextMonad-Id .introPatternM _ a = a
 
-  instance _ = Functor-M {M = M}
+module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadError (List ErrorPart) M ⦄ ⦃ mre : MonadReader TCEnv M ⦄ ⦃ _ : MonadTC M ⦄ where
 
   refineWithSingle : (Term → Term) → M Term → M Term
   refineWithSingle ref x = do
@@ -266,8 +261,6 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
 
 module ClauseExprM {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ _ : ContextMonad M ⦄ where
 
-  instance _ = Functor-M {M = M}
-
   -- Construct a ClauseExpr in M and extend the context appropriately
   matchExprM : List (SinglePattern × M (ClauseExpr ⊎ Maybe Term)) → M ClauseExpr
   matchExprM = _<$>_ MatchExpr ∘ traverse (λ (a , b) → (a ,_) <$> introPatternM a b)
@@ -321,6 +314,8 @@ clauseTelescope (Clause.clause tel _ _) = tel
 clauseTelescope (Clause.absurd-clause tel _) = tel
 
 module _ where
+  open import Class.Monad.Id
+
   open ClauseExprM ⦃ Monad-Id ⦄ ⦃ ContextMonad-Id ⦄
 
   instanciatePattern : SinglePattern → List (Arg Type)

Tactic/Derive.agda

@@ -23,7 +23,8 @@ open import Meta.Prelude
 
 open import Agda.Builtin.Reflection using () renaming (primShowQName to showName)
 
-import Data.List as L
+import Data.Bool.ListAction as L
+import Data.List as L hiding (any)
 import Data.List.NonEmpty as NE
 import Data.String as S
 open import Data.Maybe using (fromMaybe)