[Agda] This must be a type checking bug, right?

David Leduc david.leduc6 at googlemail.com
Sat Oct 2 09:29:06 CEST 2010


The simple code below fails type checking with the error message

  Failed to infer the value of dotted pattern
  when checking that the pattern ._ has type A

However if I replace "sym q" by "sym p", then it type checks!
How can I convince Agda that it is well typed?

module test where

open import Relation.Binary.PropositionalEquality

test : (A : Set)(u v : A)(p q : u ≡ v) -> A
test A u v p q rewrite p | sym q = {!!}


More information about the Agda mailing list