Closed UlfNorell closed 10 years ago
From andreas....@gmail.com on November 02, 2013 17:17:59
Fixed. I had forgotten to check for equality of projection names in the new syntactic equality check.
Summary: Error in SyntacticEquality (was: uncaught type error)
Status: Fixed
Owner: andreas....@gmail.com
Labels: Type-Defect Conversion
From sanzhi...@gmail.com on November 03, 2013 00:19:37
With latest darcs Agda the following gets accepted but "O (Γ.refl γo)" should be a type error.
record RGraph : Set₁ where field O : Set R : Set
refl : O -> R
module Families (Γ : RGraph) where
module Γ = RGraph Γ
record RG-Fam : Set₁ where field O : Γ.O -> Set
refl : ∀ {γo} -> (o : O γo) → O (Γ.refl γo)
Original issue: http://code.google.com/p/agda/issues/detail?id=933