[Agda] Type error?? But I'm sure it's well-typed!

[Andreas Abel]

"sym p" cannot be abstracted in the type of test(').  But there are  
dependencies, because if sym p is refl, p is also refl, and B is A.

Something that works is matching on p directly:

test'' : (A B : Set)(p : A ≡ B) -> T A B p -> T (T A B p) (T A B p)  
refl
test'' A .A refl (makeT a b) = {!!}

On Oct 4, 2010, at 2:45 PM, David Leduc wrote:

>
> {-# OPTIONS --universe-polymorphism #-}
>
> module test where
>
> open import Level
> open import Relation.Binary.PropositionalEquality
>
> data T {l : Level}(A B : Set l)(p : A ≡ B) : Set l where
>  makeT : A -> B -> T A B p
>
> test : (A B : Set)(p : A ≡ B) -> T A B p -> T (T A B p) (T A B p)  
> refl
> test A B p (makeT a b) rewrite sym p = {!!}
>
> test' : (A B : Set)(p : A ≡ B) -> T A B p -> T (T A B p) (T A B p)  
> refl
> test' A B p t with B | sym p
> test' A B p (makeT a b) | ._ | refl = {!!}

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/