Updated to recent Agda

Author: effectfully

src/Generic/Core.agda

@@ -56,7 +56,7 @@ mutual
 
 mutual
   Extend : ∀ {ι β} {I : Set ι} -> Desc I β -> (I -> Set β) -> I -> Set β
-  Extend (var i)   B j = Lift (i ≡ j)
+  Extend (var i)   B j = Lift _ (i ≡ j)
   Extend (π i q C) B j = Extendᵇ i C q B j
   Extend (D ⊛ E)   B j = ⟦ D ⟧ B × Extend E B j
 

src/Generic/Examples/Data/Lift.agda

@@ -3,7 +3,7 @@ module Generic.Examples.Data.Lift where
 open import Generic.Main as Main hiding (Lift; lift; lower)
 
 Lift : ∀ {α} β -> Set α -> Set (α ⊔ β)
-Lift β = readData Main.Lift
+Lift = readData Main.Lift
 
 pattern lift x = !#₀ (relv x , lrefl)
 

src/Generic/Examples/Data/Maybe.agda

@@ -5,8 +5,8 @@ open import Generic.Main as Main hiding (Maybe; just; nothing)
 Maybe : ∀ {α} -> Set α -> Set α
 Maybe = readData Main.Maybe
 
-pattern just x  = #₀ (relv x , lrefl)
-pattern nothing = !#₁ lrefl
+pattern nothing = #₀ lrefl
+pattern just x  = !#₁ (relv x , lrefl)
 
 just′ : ∀ {α} {A : Set α} -> A -> Maybe A
 just′ = just

src/Generic/Examples/Data/W.agda

@@ -2,10 +2,11 @@ module Generic.Examples.Data.W where
 
 open import Generic.Main
 
-import Data.W as W
+data W′ {α β} (A : Set α) (B : A -> Set β) : Set (α ⊔ β) where
+  sup′ : ∀ {x} -> (B x -> W′ A B) -> W′ A B
 
 W : ∀ {α β} -> (A : Set α) -> (A -> Set β) -> Set (α ⊔ β)
-W = readData W.W
+W = readData W′
 
 pattern sup x g = !#₀ (relv x , g , lrefl)
 

src/Generic/Examples/DeriveEq.agda

@@ -22,11 +22,7 @@ module DeriveEqVec where
   test₁ : xs ≟ xs ≡ yes refl
   test₁ = refl
 
-  -- Makes Agda loop?
-  -- test₂ : xs ≟ (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ no _
-  -- test₂ = refl
-
-  test₂ : xs == (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ false
+  test₂ : xs ≟ (2 ∷ᵥ 4 ∷ᵥ 2 ∷ᵥ []ᵥ) ≡ no _
   test₂ = refl
 
 module DeriveEqD where

src/Generic/Examples/Experiment.agda

@@ -81,10 +81,9 @@ module Example1 where
   find : {A : Set} {{x : A}} -> A
   find {{x}} = x
 
-  -- Looks like Agda can't find the instance because of the implicit lambda bug:
-  -- `DataEq {{find}}` doesn't work.
-  test : _≟_ {{DataEq {{λ {_} -> find}}}} arose arose ≡ yes refl
-  test = refl
+  -- -- Instance search cannot be used to find elements in an explicit function type
+  -- test : _≟_ {{DataEq {{λ {_} -> find}}}} arose arose ≡ yes refl
+  -- test = refl
 
 module Example2 where
   -- If `A` is a parameter, then this definition would be strictly positive,

src/Generic/Examples/ReadData.agda

@@ -6,7 +6,9 @@ data D {α β} (A : Set α) (B : ℕ -> Set β) : ∀ {n} -> B n -> List ℕ ->
   c₁ : ∀ {n} (y : B n) xs -> A -> D A B y xs
   c₂ : ∀ {y : B 0} -> (∀ {n} (y : B n) {{xs}} -> D A B y xs) -> .(List A) -> D A B y []
 
-D′ : TypeOf D
+-- No longer works: Failed to solve the following constraints: Has bigger sort: Setω
+-- D′ : TypeOf D
+D′ : ∀ {α β} -> (A : Set α) -> (B : ℕ -> Set β) -> ∀ {n} -> B n -> List ℕ -> Set (α ⊔ β)
 D′ = readData D
 
 unquoteDecl foldD = deriveFoldTo foldD (quote D)

src/Generic/Function/Elim.agda

@@ -23,7 +23,7 @@ varView  D      = no-var
 mutual
   Hyp : ∀ {ι β γ} {I : Set ι} {B}
       -> (∀ {i} -> B i -> Set γ) -> (D : Desc I β) -> ⟦ D ⟧ B -> Set (β ⊔ γ)
-  Hyp {β = β} C (var i)    y      = Lift {ℓ = β} (C y)
+  Hyp {β = β} C (var i)    y      = Lift β (C y)
   Hyp         C (π i q D)  f      = Hypᵇ i C D f
   Hyp         C (D ⊛ E)   (x , y) = Hyp C D x × Hyp C E y
 
@@ -38,8 +38,8 @@ mutual
        -> (D : Desc I β)
        -> (∀ {j} -> Extend D B j -> B j)
        -> Set (β ⊔ γ)
-  Elim {β = β} C (var i)   k = Lift {ℓ = β} (C (k lrefl))
-  Elim         C (π i q D) k = Elimᵇ i C D k 
+  Elim {β = β} C (var i)   k = Lift β (C (k lrefl))
+  Elim         C (π i q D) k = Elimᵇ i C D k
   Elim         C (D ⊛ E)   k with varView D
   ... | yes-var = ∀ {x} -> C x -> Elim C E (k ∘ _,_ x)
   ... | no-var  = ∀ {x} -> Hyp C D x -> Elim C E (k ∘ _,_ x)
@@ -85,7 +85,7 @@ module _ {ι β γ} {I : Set ι} {D₀ : Data (Desc I β)} (C : ∀ {j} -> μ D
                  -> (e : Extend D (μ D₀) j)
                  -> C (k e)
       elimExtend (var i)   z  lrefl  = lower z
-      elimExtend (π i q D) h  p      = elimExtendᵇ i D h p 
+      elimExtend (π i q D) h  p      = elimExtendᵇ i D h p
       elimExtend (D ⊛ E)   h (d , e) with varView D
       ... | yes-var = elimExtend E (h (elim d))  e
       ... | no-var  = elimExtend E (h (elimHyp D d)) e

src/Generic/Lib/Category.agda

@@ -5,7 +5,7 @@ open import Category.Applicative public
 open import Category.Monad public
 
 open RawFunctor {{...}} public
-open RawApplicative {{...}} hiding (_<$>_; _<$_; zipWith) renaming (_⊛_ to _<*>_) public
-open RawMonad {{...}} hiding (pure; _<$>_; _<$_; _⊛_; _<⊛_; _⊛>_; _⊗_; rawFunctor; zipWith) public
+open RawApplicative {{...}} hiding (_<$>_; _<&>_; _<$_; zip; zipWith) renaming (_⊛_ to _<*>_) public
+open RawMonad {{...}} hiding (pure; _<$>_; _<&>_; _<$_; _⊛_; _<⊛_; _⊛>_; _⊗_; rawFunctor; zip; zipWith) public
 
 fmap = _<$>_

src/Generic/Lib/Data/List.agda

@@ -27,7 +27,7 @@ mapInd f (x ∷ xs) = f 0 x ∷ mapInd (f ∘ suc) xs
 
 mapM : ∀ {α β} {A : Set α} {B : Set β} {M : Set β -> Set β} {{mMonad : RawMonad M}}
      -> (A -> M B) -> List A -> M (List B)
-mapM {{mMonad}} = List.mapM mMonad
+mapM {{mMonad}} = List.TraversableM.mapM mMonad
 
 downFromTo : ℕ -> ℕ -> List ℕ
 downFromTo n m = map (m +_) (downFrom (n ∸ m))
@@ -98,5 +98,5 @@ lookupAllConst : ∀ {α β} {A : Set α} {B : Set β} {{bEq : Eq B}} {xs : List
                -> B -> All (const B) xs -> Maybe (∃ (_∈ xs))
 lookupAllConst {xs = []}     y  tt      = nothing
 lookupAllConst {xs = x ∷ xs} y (z , ys) = if y == z
-  then just (, phere xs)
+  then just (_ , phere xs)
   else second (there xs) <$> lookupAllConst y ys