[Agda] Possibly infinite/exponential compilation time by just calling a certain function

Nils Anders Danielsson nad at cse.gu.se
Mon Jun 26 16:33:28 CEST 2017


On 2017-06-23 12:42, Jan Bracker wrote:
> What really baffles me is that these are postulates. I do not
> understand why the compiler should ever take any significant amount of
> time to check them.

I think Agda has trouble checking that the last equality type that you
give is well-formed.

I managed to get the code to type-check by adding a large number of
"abstract" annotations to your code (and postulating a single lemma that
failed to type-check), see the attached patch. I suggest that you try to
make all of your "proofs" abstract.

-- 
/NAD
-------------- next part --------------
diff --git a/src/Theory/Category/Examples.agda b/src/Theory/Category/Examples.agda
index 0d36f4f..8079942 100644
--- a/src/Theory/Category/Examples.agda
+++ b/src/Theory/Category/Examples.agda
@@ -134,6 +134,9 @@ catCategory {ℓ₀} {ℓ₁} = record
   ; left-id = left-id
   ; right-id = right-id
   } where
+
+    abstract
+
       assoc : {a b c d : Category} {f : Functor a b} {g : Functor b c} {h : Functor c d}
             → [ h ]∘[ [ g ]∘[ f ] ] ≡ [ [ h ]∘[ g ] ]∘[ f ]
       assoc = functor-eq refl refl
@@ -141,8 +144,10 @@ catCategory {ℓ₀} {ℓ₁} = record
       right-id : {a b : Category} {f : Functor a b} → [ Id[ b ] ]∘[ f ] ≡ f
       right-id = functor-eq refl refl
 
+    postulate
+
       left-id : {a b : Category} {f : Functor a b} → [ f ]∘[ Id[ a ] ] ≡ f
-    left-id = refl
+      -- left-id = refl
 
 -- Category of functors and natural transformations
 functorCategory : {Cℓ₀ Cℓ₁ Dℓ₀ Dℓ₁ : Level} → Category {Cℓ₀} {Cℓ₁} → Category {Dℓ₀} {Dℓ₁} → Category
@@ -151,10 +156,25 @@ functorCategory C D = record
   ; Hom = NaturalTransformation {C = C} {D}
   ; _∘_ = λ {F} {G} {H} → ⟨_⟩∘ᵥ⟨_⟩ {C = C} {D} {F} {G} {H}
   ; id = λ {F} → Id⟨ F ⟩
-  ; assoc = natural-transformation-eq $ fun-ext $ λ _ → Category.assoc D
-  ; left-id = natural-transformation-eq $ fun-ext $ λ _ → Category.left-id D
-  ; right-id = natural-transformation-eq $ fun-ext $ λ _ → Category.right-id D
+  ; assoc = assoc′
+  ; left-id = left-id′
+  ; right-id = right-id′
   }
+  where
+  abstract
+
+    assoc′ : {a b c d : Functor C D} {f : NaturalTransformation a b}
+             {g : NaturalTransformation b c} {h : NaturalTransformation c d} →
+             ⟨ h ⟩∘ᵥ⟨ ⟨ g ⟩∘ᵥ⟨ f ⟩ ⟩ ≡ ⟨ ⟨ h ⟩∘ᵥ⟨ g ⟩ ⟩∘ᵥ⟨ f ⟩
+    assoc′ = natural-transformation-eq $ fun-ext $ λ _ → Category.assoc D
+
+    left-id′ : {a b : Functor C D} {f : NaturalTransformation a b} →
+               ⟨ f ⟩∘ᵥ⟨ Id⟨ a ⟩ ⟩ ≡ f
+    left-id′ = natural-transformation-eq $ fun-ext $ λ _ → Category.left-id D
+
+    right-id′ : {a b : Functor C D} {f : NaturalTransformation a b} →
+                ⟨ Id⟨ b ⟩ ⟩∘ᵥ⟨ f ⟩ ≡ f
+    right-id′ = natural-transformation-eq $ fun-ext $ λ _ → Category.right-id D
 
 [_,_] = functorCategory
 
diff --git a/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda b/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
index 11f847c..8cd8162 100644
--- a/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
+++ b/src/Theory/Category/Monoidal/Examples/FunctorWithDayConvolution/Postulates.agda
@@ -42,9 +42,7 @@ postulate
 
   dayRightUnitor : {ℓC₀ ℓC₁ : Level} → (ℓSet : Level) → {C : Category {ℓC₀} {ℓC₁}} → (CMon : MonoidalCategory C)
                  → NaturalIsomorphism ([-, dayUnit {ℓSet = ℓSet} CMon ] (dayConvolution {ℓSet = ℓSet} CMon)) Id[ FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁}) ]
-  {-
   day-triangle-id : {ℓC₀ ℓC₁ : Level} → (ℓSet : Level) → {C : Category {ℓC₀} {ℓC₁}} → (CMon : MonoidalCategory C)
                   → (x y : Functor C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁}))
                   → F₁ (dayConvolution {ℓSet = ℓSet} CMon) (iso-η (dayRightUnitor ℓSet CMon) x , id (FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁})) {y} )
                   ≡ ⟨ F₁ (dayConvolution {ℓSet = ℓSet} CMon) (id (FunCat C (setCategory {ℓSet ⊔ ℓC₀ ⊔ ℓC₁})) {x} , iso-η (dayLeftUnitor ℓSet CMon) y) ⟩∘ᵥ⟨ iso-η (dayAssociator ℓSet CMon) (x ,' dayUnit {ℓSet = ℓSet} CMon ,' y) ⟩
-  -}
diff --git a/src/Theory/End/Convolution.agda b/src/Theory/End/Convolution.agda
index b63e479..9f553f5 100644
--- a/src/Theory/End/Convolution.agda
+++ b/src/Theory/End/Convolution.agda
@@ -41,6 +41,8 @@ convolutionFunctor {ℓC₀} {ℓC₁} {ℓSet} {C} CMon (functor F₀ F₁ F-id
     dayF₁ : {a b : Obj CC×CC} → Hom CC×CC a b → Hom Set' (dayF₀ a) (dayF₀ b)
     dayF₁ {a} {b} ((f₁ , f₁') , (f₂ , f₂')) (homC , Fc , Fc') = (homC ∘C (f₁ ⊗C₁ f₁')) , F₁ f₂ Fc , G₁ f₂' Fc'
 
+    abstract
+
       day-id : {a : Obj CC×CC} → dayF₁ {a} {a} (id CC×CC) ≡ id Set'
       day-id {a} = begin
         dayF₁ {a} {a} (id CC×CC)
@@ -99,6 +101,8 @@ convolutionTransformation {ℓC₀} {ℓC₁} {ℓSet} {C} CMon {F} {G} {F'} {G'
     η : (x' : Obj CC×CC) → Hom Set' ([ convolutionFunctor {ℓSet = ℓSet} CMon F G a ]₀ x') ([ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₀ x')
     η ((c₀⁻ , c₁⁻) , (c₀⁺ , c₁⁺)) (f , Fc₀ , Gc₁) = (g ∘C f) , nat-η α c₀⁺ Fc₀ , nat-η β c₁⁺ Gc₁
 
+    abstract
+
       nat : {x y : Obj CC×CC} {f : Hom CC×CC x y} → [ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₁ f ∘F η x ≡ η y ∘F [ convolutionFunctor {ℓSet = ℓSet} CMon F G a ]₁ f
       nat {x} {y} {f} = begin
         [ convolutionFunctor {ℓSet = ℓSet} CMon F' G' b ]₁ f ∘F η x
@@ -123,7 +127,8 @@ convolutionTransFun : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {
                     → NaturalTransformation (convolutionFunctor {ℓSet = ℓSet} CMon F G x) (convolutionFunctor {ℓSet = ℓSet} CMon F' G' x)
 convolutionTransFun {ℓC₀} {ℓC₁} {ℓSet} {C} CMon α β x = convolutionTransformation {ℓSet = ℓSet} CMon α β (Category.id C {x})
 
-convolution-trans-obj-id : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {ℓC₁}} (CMon : MonoidalCategory C) 
-                         → (F G : Functor C (setCategory {ℓSet ⊔ ℓC₁ ⊔ ℓC₀})) → (a : Obj C) → convolutionTransObj {ℓSet = ℓSet} CMon F G (id C {a}) ≡ Id⟨ convolutionFunctor {ℓSet = ℓSet} CMon F G a ⟩
-convolution-trans-obj-id {ℓC₀} {ℓC₁} {ℓSet} {C} CMon F G a = natural-transformation-eq $ fun-ext $ λ (c : Obj ((C ×C C) op ×C (C ×C C))) → fun-ext (λ {(f , Fc , Gc) → cong (λ X → X , Fc , Gc) (right-id C)})
+abstract
 
+  convolution-trans-obj-id : {ℓC₀ ℓC₁ ℓSet : Level} {C : Category {ℓC₀} {ℓC₁}} (CMon : MonoidalCategory C)
+                           → (F G : Functor C (setCategory {ℓSet ⊔ ℓC₁ ⊔ ℓC₀})) → (a : Obj C) → convolutionTransObj {ℓSet = ℓSet} CMon F G (id C {a}) ≡ Id⟨ convolutionFunctor {ℓSet = ℓSet} CMon F G a ⟩
+  convolution-trans-obj-id {ℓC₀} {ℓC₁} {ℓSet} {C} CMon F G a = natural-transformation-eq $ fun-ext $ λ (c : Obj ((C ×C C) op ×C (C ×C C))) → fun-ext (λ {(f , Fc , Gc) → cong (λ X → X , Fc , Gc) (right-id C)})
diff --git a/src/Theory/End/DayConvolution.agda b/src/Theory/End/DayConvolution.agda
index 5cff565..afc6c83 100644
--- a/src/Theory/End/DayConvolution.agda
+++ b/src/Theory/End/DayConvolution.agda
@@ -67,6 +67,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
         d0₁ : {a b : Obj C} → Hom C a b → Hom Set' (Set-co-∫ ℓSet (dayF F G a)) (Set-co-∫ ℓSet (dayF F G b))
         d0₁ {a} {b} f = coendMorph (convolutionTransObj F G f)
 
+        abstract
+
           d0-id : {a : Obj C} → d0₁ {a} {a} (id C) ≡ id Set'
           d0-id {a} = begin
             coendMorph (convolutionTransObj F G (id C))
@@ -88,6 +90,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
         day-η : (x : Obj C) → Hom Set' (CoEnd.co-∫ (dayEnd F G x)) (CoEnd.co-∫ (dayEnd F' G' x))
         day-η x = coendMorph (convolutionTransFun α β x)
 
+        abstract
+
           day-nat : {x y : Obj C} {f : Hom C x y} → [ day₀ (F' , G') ]₁ f ∘F day-η x ≡ day-η y ∘F [ day₀ (F , G) ]₁ f
           day-nat {x} {y} {f} = begin
             [ day₀ (F' , G') ]₁ f ∘F day-η x
@@ -100,6 +104,8 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
               ≡⟨⟩
             day-η y ∘F [ day₀ (F , G) ]₁ f ∎
 
+    abstract
+
       day-id : {a : Obj [C,S]×[C,S]} → day₁ {a} {a} (id [C,S]×[C,S] {a}) ≡ id [ C , Set' ] {day₀ a}
       day-id {F , G} = natural-transformation-eq $ fun-ext $ λ (c : Obj C) → begin
         coendMorph (convolutionTransFun Id⟨ F ⟩ Id⟨ G ⟩ c)
@@ -117,4 +123,3 @@ dayConvolution {ℓC₀} {ℓC₁} {ℓSet} {C} CMon = functor day₀ day₁ (λ
         coendMorph (convolutionTransFun γ δ c) ∘F coendMorph (convolutionTransFun α β c)
           ≡⟨⟩
         nat-η (day₁ {F' , G'} {F'' , G''} (γ , δ) ∘[C,S] day₁ {F , G} {F' , G'} (α , β)) c ∎
-
diff --git a/src/Theory/End/Properties.agda b/src/Theory/End/Properties.agda
index 97f68a7..6e0898a 100644
--- a/src/Theory/End/Properties.agda
+++ b/src/Theory/End/Properties.agda
@@ -34,6 +34,8 @@ wedgeTransform {ℓC₀} {ℓC₁} {ℓS} {C} {functor H₀ H₁ H-id H-comp} {f
     f' : (c : Obj C) → Hom Set' w (H'₀ (c , c))
     f' c = nat-η θ (c , c) ∘F f c
 
+    abstract
+
       coher' : {c c' : Obj C} (g : Hom C c c') → H'₁ (g , id C) ∘F f' c' ≡ H'₁ (id C , g) ∘F f' c
       coher' {c} {c'} g = begin
         H'₁ (g , id C) ∘F f' c'
@@ -59,6 +61,8 @@ cowedgeTransform {ℓC₀} {ℓC₁} {ℓS} {C} {functor H₀ H₁ H-id H-comp}
     f' : (c : Obj C) → Hom Set' (H₀ (c , c)) w
     f' c = f c ∘F nat-η θ (c , c)
 
+    abstract
+
       coher' : {c c' : Obj C} (g : Hom C c c') → f' c' ∘F H₁ (id C , g) ≡ f' c ∘F H₁ (g , id C)
       coher' {c} {c'} g = begin
         f' c' ∘F H₁ (id C , g)
@@ -83,7 +87,9 @@ coendMorph : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}}
            → Hom (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS}) (Set-co-∫ ℓS H) (Set-co-∫ ℓS H')
 coendMorph {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
 
-coend-morph-unique : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}} 
+abstract
+
+  coend-morph-unique : {ℓC₀ ℓC₁ ℓS : Level} {C : Category {ℓC₀} {ℓC₁}}
                      → {H H' : Functor (C op ×C C) (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS})} → (θ : NaturalTransformation H H')
                      → (f : Hom (setCategory {ℓC₀ ⊔ ℓC₁ ⊔ ℓS}) (Set-co-∫ ℓS H) (Set-co-∫ ℓS H')) → f ≡ coendMorph θ
-coend-morph-unique {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ proj₂ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
+  coend-morph-unique {ℓC₀} {ℓC₁} {ℓS} {C} {H} {H'} θ = proj₁ $ proj₂ $ CoEnd.co-universal (setCoEnd ℓS H) $ cowedgeTransform {ℓS = ℓS} θ $ CoEnd.co-e $ setCoEnd ℓS H'
diff --git a/src/Theory/Functor/Application.agda b/src/Theory/Functor/Application.agda
index eb452c1..c5950ec 100644
--- a/src/Theory/Functor/Application.agda
+++ b/src/Theory/Functor/Application.agda
@@ -50,6 +50,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ : Level}
       HomF : {a b : Obj D} → Hom D a b → Hom E (ObjF a) (ObjF b)
       HomF f = F₁ (id C {x} , f)
 
+      abstract
+
         composeF : {a b c : Obj D} {f : Hom D a b} {g : Hom D b c}
                  → HomF (g ∘D f) ≡ HomF g ∘E HomF f
         composeF {a} {b} {c} {f} {g} = begin
@@ -68,6 +70,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ : Level}
       HomF : {a b : Obj C} → Hom C a b → Hom E (ObjF a) (ObjF b)
       HomF f = F₁ (f , id D {x})
 
+      abstract
+
         composeF : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c}
                  → HomF (g ∘C f) ≡ HomF g ∘E HomF f
         composeF {a} {b} {c} {f} {g} = begin
diff --git a/src/Theory/Functor/Association.agda b/src/Theory/Functor/Association.agda
index ab82738..b8188b4 100644
--- a/src/Theory/Functor/Association.agda
+++ b/src/Theory/Functor/Association.agda
@@ -58,6 +58,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
       F₁ : {a b : Obj (C ×C (D ×C E))} → Hom (C ×C (D ×C E)) a b → Hom K (F₀ a) (F₀ b)
       F₁ (c , d×e) = [ C×J→K ]₁ (c , [ D×E→J ]₁ d×e)
 
+      abstract
+
         idF : {a : Obj (C ×C (D ×C E))}
             → F₁ {a} {a} (id (C ×C (D ×C E))) ≡ id K
         idF {a} = begin
@@ -72,6 +74,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
       private
         _∘CDE_ = _∘_ (C ×C (D ×C E))
 
+      abstract
+
         composeF : {a b c : Obj (C ×C (D ×C E))} {f : Hom (C ×C (D ×C E)) a b} {g : Hom (C ×C (D ×C E)) b c}
                  → F₁ (((C ×C (D ×C E)) ∘ g) f) ≡ (K ∘ F₁ g) (F₁ f)
         composeF {f = fC , fDE} {g = gC , gDE} = begin
@@ -96,6 +100,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
       F₁ : {a b : Obj ((C ×C D) ×C E)} → Hom ((C ×C D) ×C E) a b → Hom K (F₀ a) (F₀ b)
       F₁ (c×d , e) = [ J×E→K ]₁ ([ C×D→J ]₁ c×d , e)
 
+      abstract
+
         idF : {a : Obj ((C ×C D) ×C E)}
             → F₁ {a} {a} (id ((C ×C D) ×C E)) ≡ id K
         idF {a} = begin
@@ -110,6 +116,8 @@ module BiFunctor {ℓC₀ ℓC₁ ℓD₀ ℓD₁ ℓE₀ ℓE₁ ℓJ₀ ℓJ
       private
         _∘CDE_ = _∘_ ((C ×C D) ×C E)
 
+      abstract
+
         composeF : {a b c : Obj ((C ×C D) ×C E)} {f : Hom ((C ×C D) ×C E) a b} {g : Hom ((C ×C D) ×C E) b c}
                  → F₁ (g ∘CDE f) ≡ (F₁ g) ∘K (F₁ f)
         composeF {f = fCD , fE} {g = gCD , gE} = begin
@@ -140,4 +148,3 @@ module Associator {ℓC₀ ℓC₁ : Level} {C : Category {ℓC₀} {ℓC₁}} w
   -- (_ ⊗ (_ ⊗ _)) ⇒ _
   rightAssociator : Functor (C ×C C) C → Functor (C ×C C ×C C) C
   rightAssociator F = [ biAssocFunctorR F F ]∘[ assocFunctorR ]
- 
diff --git a/src/Theory/Functor/Composition.agda b/src/Theory/Functor/Composition.agda
index ecc2624..b514152 100644
--- a/src/Theory/Functor/Composition.agda
+++ b/src/Theory/Functor/Composition.agda
@@ -27,6 +27,8 @@ compFunctor {C = C} {D = D} {E = E} F G = record
     F₁ : {a b : Obj C} → Hom C a b → Hom E (F₀ a) (F₀ b)
     F₁ f = [ F ]₁ ( [ G ]₁ f )
 
+    abstract
+
       id : ∀ {a : Obj C} → F₁ {a = a} (Category.id C) ≡ Category.id E
       id = trans (cong (λ X → Functor.F₁ F X) (Functor.id G)) (Functor.id F)
 
diff --git a/src/Theory/Functor/Examples/HomFunctor.agda b/src/Theory/Functor/Examples/HomFunctor.agda
index 9fa8b2b..9e6bde9 100644
--- a/src/Theory/Functor/Examples/HomFunctor.agda
+++ b/src/Theory/Functor/Examples/HomFunctor.agda
@@ -30,6 +30,8 @@ homFunctor {ℓC₀} {ℓC₁} ℓSet {C} a = functor HomF₀ HomF₁ id-HomF co
     HomF₁ : {x y : Obj C} → Hom C x y → Hom SetCat (HomF₀ x) (HomF₀ y)
     HomF₁ f = λ g → lift (f ∘C lower g)
 
+    abstract
+
       id-HomF : {a : Obj C} → HomF₁ (id C {a}) ≡ id SetCat
       id-HomF {a} = begin
         HomF₁ (id C)
@@ -50,4 +52,3 @@ homFunctor {ℓC₀} {ℓC₁} ℓSet {C} a = functor HomF₀ HomF₁ id-HomF co
         ( λ h → lift (g ∘C (f ∘C lower h)) )
           ≡⟨⟩
         (HomF₁ g) ∘Set (HomF₁ f) ∎
- 
diff --git a/src/Theory/Natural/Transformation.agda b/src/Theory/Natural/Transformation.agda
index db4a060..065c7de 100644
--- a/src/Theory/Natural/Transformation.agda
+++ b/src/Theory/Natural/Transformation.agda
@@ -66,6 +66,8 @@ compNaturalTransformationVert {C = C} {D} {F} {G} {H} α β =  record
     η :  (a : Category.Obj C) → Category.Hom D ([ F ]₀ a) ([ H ]₀ a)
     η a = ηα a ∘D ηβ a
 
+    abstract
+
       natural : {a b : Category.Obj C} {f : Category.Hom C a b}
               → ([ H ]₁ f) ∘D (η a) ≡ (η b) ∘D ([ F ]₁ f)
       natural {a} {b} {f} = begin


More information about the Agda mailing list