internal error at MetaVars.hs:897

[UlfNorell]

From sanzhi...@gmail.com on October 27, 2013 22:11:37

Using darcs Agda, the following code triggers an internal error at src/full/Agda/TypeChecking/MetaVars.hs:897

postulate Σ : (A : Set) (B : A → Set) -> Set

<,> : {A : Set} {B : A → Set} {C : ∀ {x} → B x → Set} (f : (x : A) → B x) → ((x : A) → C (f x)) → ((x : A) → Σ (B x) C)

record ⟶ (From To : Set) : Set where field .app : From -> To

open ⟶ public

.⟪,⟫ : ∀ {From To₁ To₂ : Set} -> (From ⟶ To₁) -> (From ⟶ To₂) → From → Σ To₁ (\ _ -> To₂) ⟪ f₁ , f₂ ⟫ = < app f₁ , app f₂ >

Original issue: http://code.google.com/p/agda/issues/detail?id=927

[UlfNorell]

From nils.anders.danielsson on October 29, 2013 05:58:15

The code above was at first accepted for me, but I could reproduce the problem after pulling Andreas' last 60 patches.

Status: Accepted
Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Milestone-2.3.4

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 08:01:58

I think this has to do with the different handling of irrelevant projections I had to introduce during my big refactoring. Looking into this...

Labels: Irrelevance Meta Projection

[UlfNorell]

From andreas....@gmail.com on October 29, 2013 08:50:41

Fixed. This was just a false alarm, i.e., an IMPOSSIBLE that is now possible.

Thanks for posting this bug report.

Status: Fixed