UlfNorell
commented
10 years ago From andreas....@gmail.com on October 14, 2013 05:49:43
That was quite a riddle to solve.
- The internal error is actually triggered in the termination checking phase. I fixed this, will push soon. A workaround is --no-termination-check
- The data-Tm-brace puts ctx-hom and ctx-hom-split-iso into a mutual block. This prevents ctx-hom to be unfolded during checking the -split-iso. You can achieve the same by explicitely putting the two defs into a mutual block. If the mutual block is removed, the yellow stuff appears. HO-unification is sensitive to reduction, at this moment I do not see an easy fix for this behavior.
- "yellow spots reappear, but in different places" I could not replay this. For me, the yellow only disappeared if I also gave {T = T}, but then it consistently disappears and reappears when putting in and out of a mutual block.
Status: Accepted
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Termination Projection
From sattler....@gmail.com on October 11, 2013 02:33:49
This is a funny one. The below code snippet produces the following error under the current Agda development version:
An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Eliminators.hs:85
Note the spurious Tm datatype that isn't used anywhere? Remove it, move its declaration forward, or its definition backward, and the internal error vanishes, leaving a few yellow spots.
Now uncomment the two implicit arguments at the bottom of the code. All metavars are now resolved. Now put the Tm datatype back in - yellow spots reappear, but different from before!
{-# OPTIONS --without-K #-} module Canonicity.InHouse.Bug where
record ⊤ : Set where constructor tt
record Σ (A : Set) (B : A → Set) : Set where constructor , field proj₁ : A proj₂ : B proj₁
data ℕ : Set where zero : ℕ suc : ℕ → ℕ
∘ : {A B C : Set} → (B → C) → (A → B) → A → C g ∘ f = λ x → g (f x)
+' : ℕ → ℕ → ℕ i +' zero = i i +' suc j = suc i +' j
U : ℕ → Set U zero = ⊤ U (suc n) = Σ (U n) (λ _ → ⊤)
V : ℕ → Set V zero = ⊤ V (suc m) = Σ ⊤ (λ _ → V m)
combine : {i j : ℕ} → Σ (U i) (λ → V j) → U (i +' j) combine {j = zero} = λ {(A , ) → A} combine {j = suc j} = combine {j = j} ∘ (λ {(Γ , (A , T)) → ((Γ , A) , T)})
data Tm : Set
ctx-hom : (m : ℕ) → U m → Set ctx-hom zero = ⊤ ctx-hom (suc m) (Δ , ) = Σ (ctx-hom m Δ) (λ _ → ⊤)
ctx-hom-split-iso : {m k : ℕ} {Δ : U m} {T : V k} → ctx-hom (m +' k) (combine (Δ , T)) → Σ (ctx-hom m Δ) (λ _ → V k) ctx-hom-split-iso {k = zero} = λ Δ → (Δ , tt) ctx-hom-split-iso {m} {k = suc k} {Δ} {(A , T)} = (λ {((Γ , A) , T) → (Γ , (A , T))}) ∘ ctx-hom-split-iso --{m = suc m} {Δ = (Δ , A)}
data Tm where
Original issue: http://code.google.com/p/agda/issues/detail?id=918