Update to Agda 2.6.3

Author: WhatisRT

Diff for: .github/workflows/ci.yml

@@ -10,8 +10,8 @@ jobs:
       - uses: actions/[email protected]
       - uses: omelkonian/setup-agda@master
         with:
-          agda-version: 2.6.2.1
-          stdlib-version: 1.7
+          agda-version: 2.6.3
+          stdlib-version: 1.7.2
           main: Main
           deploy: ${{ github.ref == 'refs/heads/master' }}
           token: ${{ secrets.GITHUB_TOKEN }}

Diff for: Class/MonadTC.agda

@@ -37,8 +37,8 @@ record TCEnv : Set where
     reconstruction : Bool
     noConstraints  : Bool
     reduction      : ReductionOptions
-    globalContext  : List $ Arg Type
-    localContext   : List $ Abs $ Arg Type
+    globalContext  : Telescope
+    localContext   : Telescope
     goal           : Term ⊎ Type
     debug          : DebugOptions
 
@@ -236,21 +236,21 @@ module _ {M : ∀ {f} → Set f → Set f}
       isAppliedToUnknownsAndMetas (meta x args)     = isUnknownsAndMetas args
       isAppliedToUnknownsAndMetas _                 = true
 
-  extendContext : Arg Type → M A → M A
-  extendContext ty = local λ where e@record { localContext = Γ } → record e { localContext = abs "" ty ∷ Γ }
+  extendContext : String × Arg Type → M A → M A
+  extendContext ty = local λ where e@record { localContext = Γ } → record e { localContext = ty ∷ Γ }
 
-  getContext : M $ List $ Arg Type
+  getContext : M Telescope
   getContext = reader λ where
-    e@record { localContext = Γ ; globalContext = Γ' } → map unAbs Γ Data.List.++ Γ'
+    e@record { localContext = Γ ; globalContext = Γ' } → Γ Data.List.++ Γ'
 
-  getLocalContext : M $ List $ Arg Type
-  getLocalContext = reader λ where e@record { localContext = Γ } → map unAbs Γ
+  getLocalContext : M Telescope
+  getLocalContext = reader λ where e@record { localContext = Γ } → Γ
 
-  inContext : List $ Arg Type → M A → M A
-  inContext ctx = local λ e → record e { localContext = map (abs "") ctx }
+  inContext : Telescope → M A → M A
+  inContext ctx = local λ e → record e { localContext = ctx }
 
   -- extend context by multiple variables
-  extendContext' : List (Arg Type) → M A → M A
+  extendContext' : Telescope → M A → M A
   extendContext' [] x = x
   extendContext' (c ∷ cs) x = extendContext c (extendContext' cs x)
 
@@ -311,8 +311,8 @@ module _ {M : ∀ {f} → Set f → Set f}
   getConstrsForTerm t = getConstrsForType =<< inferType t
 
   -- run a TC computation to arrive at the term under the binder for the pattern
-  withPattern : List (String × Arg Type) → List (Arg Pattern) → M Term → M Clause
-  withPattern tel ps t = Clause.clause tel ps <$> extendContext' (map proj₂ tel) t
+  withPattern : Telescope → List (Arg Pattern) → M Term → M Clause
+  withPattern tel ps t = Clause.clause tel ps <$> extendContext' tel t
 
   unifyWithGoal : Term → M ⊤
   unifyWithGoal t = do

Diff for: Generics/Debug.agda

@@ -20,7 +20,7 @@ open import Reflection.Meta
 
 open import Class.Show.Core
 open import Class.Show.Instances
-open import Class.Functor.Instances
+open import Class.Functor
 open import Class.Monad
 open import Class.Traversable.Core
 open import Class.Traversable.Instances
@@ -74,7 +74,7 @@ module Debug (v : String × ℕ) where
       go (i , ty) = print $ "\t" Str.++ show i Str.++ " : " Str.++ show ty
 
   printCurrentContext : TC ⊤
-  printCurrentContext = printContext =<< getContext
+  printCurrentContext = printContext =<< (Data.List.map proj₂ <$> getContext)
 
   -- ** definitions
   genSimpleDef : Name → Type → Term → TC ⊤

Diff for: Reflection/TCI.agda

@@ -50,13 +50,13 @@ applyNoConstraints : TC A → TC A
 applyNoConstraints x r@record { noConstraints = false } = x r
 applyNoConstraints x r@record { noConstraints = true  } = R'.noConstraints (x r)
 
-applyExtContext : List (Arg Term) → R.TC A → R.TC A
+applyExtContext : Telescope → R.TC A → R.TC A
 applyExtContext [] x       = x
-applyExtContext (t ∷ ts) x = applyExtContext ts $ R.extendContext t x
+applyExtContext (t ∷ ts) x = applyExtContext ts $ (uncurry R.extendContext) t x
 
 private
   liftTC : R.TC A → TC A
-  liftTC x = λ r → applyExtContext (map unAbs $ r .TCEnv.localContext) x
+  liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x
 
   liftTC1 : (A → R.TC B) → A → TC B
   liftTC1 f a = liftTC (f a)

Diff for: Tactic/ClauseBuilder.agda

@@ -103,7 +103,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
   ctxSinglePatterns : M (List SinglePattern)
   ctxSinglePatterns = do
     ctx ← getContext
-    return (singlePatternFromPattern <$> zipWithIndex (λ where k (arg i _) → arg i (` k)) ctx)
+    return (singlePatternFromPattern <$> zipWithIndex (λ where k (_ , (arg i _)) → arg i (` k)) ctx)
 
   -- TODO: add the ability to match initial hidden arguments
   -- TODO: add dot patterns
@@ -243,7 +243,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
   isProj _                = false
 
   -- if the goal is of type (a : A) → B, return the type of the branch of pattern p and new context
-  specializeType : SinglePattern → Type → M (Type × List (Arg Type))
+  specializeType : SinglePattern → Type → M (Type × Telescope)
   specializeType p@(t , arg i p') goalTy = markDontFail "specializeType" $ inDebugPath "specializeType" $ runAndReset do
     debugLog ("Goal type to specialize: " ∷ᵈ goalTy ∷ᵈ [])
     cls@((Clause.clause tel _ _) ∷ _) ← return $ clauseExprToClauses $ MatchExpr $
@@ -256,12 +256,10 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
                   ∷ᵈ "\nWith type:" ∷ᵈ goalTy ∷ᵈ "\nSinglePattern:" -- ∷ᵈ {!p!}
                   ∷ᵈ []) >> error1 "BUG"
     let varsToUnbind = 0
-    let newCtx = proj₂ <$> tel'
+    let newCtx = tel'
     let m = meta x (map-Args (mapVars (_∸ varsToUnbind)) $ take (length ap ∸ varsToUnbind) ap)
-    logCurrentContext
     debugLog1 "New context:"
-    logTelescope (Data.List.map (nothing ,_) newCtx)
-    debugLog1 "TEST"
+    logContext newCtx
     goalTy' ← extendContext' newCtx $ inferType m
     return (goalTy' , newCtx)
 

Diff for: Tactic/Derive.agda

@@ -61,7 +61,7 @@ genClassType arity dName wName = do
     adjustParams [] = return []
     adjustParams (abs x (arg _ t) ∷ l) = do
       a ← (if_then [ (abs "_" (iArg (className ∙⟦ ♯ 0 ⟧)) , false) ] else []) <$> isNArySort arity t
-      ps ← extendContext (hArg t) (adjustParams l)
+      ps ← extendContext (x , hArg t) (adjustParams l)
       let ps' = flip L.map ps λ where
         (abs s (arg i t) , b) → (abs s (arg i (mapVars (_+ (if b then length a else 0)) t)) , b)
       return (((abs x (hArg t) , true) ∷ a) ++ ps')

Diff for: Tactic/Helpers.agda

@@ -60,9 +60,9 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
           (just "") → "_"
           (just x)  → x
         debugLog ("  " ∷ᵈ name ∷ᵈ " : "  ∷ᵈ mapVars (_∸ (n ∸ (1 + length l))) t ∷ᵈ [])
-        extendContext ty $ helper n l
+        extendContext (name , ty) $ helper n l
 
-  logContext : List $ Arg Type → M ⊤
+  logContext : Telescope → M ⊤
   logContext l = withAppendDebugPath "context" do
     debugLog1 "Context:"
     catch (helper (length l) l) (λ _ → debugLog1 "Error while printing the context!")
@@ -74,9 +74,9 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
           where _ → error1 "Bug in logContext!"
         debugLog ("Error while infering the goal type! Goal: " ∷ᵈ t ∷ᵈ [])
     where
-      helper : ℕ → List $ Arg Type → M ⊤
+      helper : ℕ → Telescope → M ⊤
       helper n [] = return _
-      helper n (arg _ t ∷ l) = do
+      helper n ((_ , arg _ t) ∷ l) = do
         helper n l
         debugLog ("  " ∷ᵈ ♯ (n ∸ (length l + 1)) ∷ᵈ " : " ∷ᵈ mapVars (_+ (n ∸ length l)) t ∷ᵈ [])
 
@@ -95,7 +95,7 @@ module _ {M : ∀ {a} → Set a → Set a} ⦃ _ : Monad M ⦄ ⦃ me : MonadErr
       helper : Type → ℕ → M TypeView
       helper ty    zero = return $ viewTy ty
       helper ty (suc k) with viewTy ty
-      ... | (tel , ty') = extendContext' (map unAbs tel) $ do
+      ... | (tel , ty') = extendContext' (map (λ where (abs s t) → s , t) tel) $ do
         rTy ← reduce ty'
         (tel' , rTy') ← helper rTy k
         return (tel ++ tel' , rTy')

Diff for: Tactics/Existentials.agda

@@ -25,9 +25,6 @@ mkExistential lvl t = do
     go n₀ (suc n) = quote ∃ ∙⟦ (`λ "_" ⇒ go n₀ n) ⟧
 
 macro
-  mk∃[nest:_] : ℕ → Name → Tactic
-  mk∃[nest:_] lvl t hole = mkExistential lvl t >>= unify hole
-
   mk∃ : Name → Tactic
   mk∃ t hole = mkExistential 0 t >>= unify hole
 
@@ -42,18 +39,18 @@ private
     data Y : String → ℕ → Set where
       mkY : Y "" 1
 
-    _ : mk∃[nest: 1 ] Y
+    _ : mk∃ Y
     _ = "" , 1 , mkY
 
     module _ (s : String) where
 
       data Z : ℕ → Set where
         mkZ : Z 1
 
-      _ : mk∃[nest: 2 ] Z
+      _ : mk∃ Z
       _ = 1 , mkZ
 
-    _ : mk∃[nest: 1 ] Z
+    _ : mk∃ Z
     _ = "sth" , 1 , mkZ
 
   _ : mk∃ Y

Diff for: Tactics/Intro.agda

@@ -24,11 +24,11 @@ intro hole k = do
   case ty of λ where
     (pi argTy@(arg (arg-info v _) _) (abs x ty′)) → do
       ctx ← getContext
-      hole′ ← inContext (argTy ∷ ctx) $ do
+      hole′ ← inContext (("" , argTy) ∷ ctx) $ do
         hole′ ← newMeta ty′
         return hole′
       unifyStrict (hole , ty) (lam v (abs "_" hole′))
-      extendContext argTy $ do
+      extendContext x argTy $ do
         k hole′
     _ → k hole
 
@@ -37,15 +37,15 @@ intros : Hole → Tactic → TC ⊤
 intros hole k = do
   ty ← inferType hole
   case ty of λ where
-    (pi argTy@(arg (arg-info v _) _) (abs _ ty′)) → do
+    (pi argTy@(arg (arg-info v _) _) (abs x ty′)) → do
       ctx ← getContext
       print $ "\t* " ◇ show argTy
-      printContext ctx
-      hole′ ← inContext (argTy ∷ ctx) $ do
+      printCurrentContext
+      hole′ ← inContext ((x , argTy) ∷ ctx) $ do
         hole′ ← newMeta ty′
         return hole′
       unifyStrict (hole , ty) (lam v (abs "_" hole′))
-      extendContext argTy $ do
+      extendContext x argTy $ do
         intros hole′ k
     _ → k hole
 
@@ -54,7 +54,7 @@ private
   fillFromContext hole = do
     ty ← inferType hole
     ctx ← getContext
-    printContext ctx
+    printCurrentContext
     let n = length ctx
     let vs = applyUpTo ♯ n
     unifyStricts (hole , ty) vs
@@ -119,8 +119,8 @@ private
   _ : ∀ {n : Bool} → Bool
   _ = intros→fill
 
-  _ : {n : ℕ} (b : Bool) → Bool
-  _ = intros→fill
+  -- _ : {n : ℕ} (b : Bool) → Bool
+  -- _ = intros→fill
 
   _ : (n : ℕ) → Bool → Bool
   _ = intros→fill
@@ -131,19 +131,19 @@ private
   _ : (b : Bool) {n : ℕ} → ℕ
   _ = intros→fill
 
-  _ : ∀ {b : Bool} (n : ℕ) → ℕ
-  _ = intros→fill
+  -- _ : ∀ {b : Bool} (n : ℕ) → ℕ
+  -- _ = intros→fill
 
   _ : ∀ (b : Bool) (n : ℕ) → Bool
   _ = intros→fill
 
   open import Data.List.Membership.Propositional
 
-  _ : ∀ {x : ℕ} {xs} → x ∈ xs → x ∈ xs
-  _ = intro→fill
+  -- _ : ∀ {x : ℕ} {xs} → x ∈ xs → x ∈ xs
+  -- _ = intro→fill
 
-  _ : ∀ {x y : ℕ} {xs ys} → x ∈ xs → y ∈ ys → x ∈ xs
-  _ = intros→fill
+  -- _ : ∀ {x y : ℕ} {xs ys} → x ∈ xs → y ∈ ys → x ∈ xs
+  -- _ = intros→fill
 
-  _ : ∀ {x y : ℕ} {xs} → x ∈ xs → y ∈ xs → y ∈ xs
-  _ = intros→fill
+  -- _ : ∀ {x y : ℕ} {xs} → x ∈ xs → y ∈ xs → y ∈ xs
+  -- _ = intros→fill

Diff for: Tactics/Try.agda

@@ -217,13 +217,13 @@ tryWith userDB f₀ hole₀ = do
   (f , fTy) ← viewTerm f₀
   print $ show f ◇ " : " ◇ show fTy
   ctx ← getContext
-  prints "ctx" ctx
+  printCurrentContext
   let
     db : List Term
     db = nodup
        $ map ♯ (upTo $ length ctx)
       ++ subterms holeTy
-      ++ subterms ctx
+      ++ subterms (map proj₂ ctx)
       ++ userDB
       ++ [ unknown ]
   prints "db" db