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

[Nils Anders Danielsson]

On 2010-10-04 13:45, David Leduc wrote:
> Why the function "test" below is rejected by the type-checker?

Try writing out the code generated by with (use -vtc.with.top:20):

   test A B p (makeT a b) = rewrite-18 A B p B (sym p) a b

   rewrite-18 :
     (A B : Set) (p : A ≡ B) (w : Set) (w' : w ≡ A) (a : A) (b : w) →
     T (T A w p) (T A w p) (refl {_} {_} {_})
   <No body is generated, because the type signature is incorrect.>

Note that the type of p is incorrect in the codomain of rewrite-18: p
doesn't have type A ≡ w. This explains the error message:

   B != w of type Set
   when checking that the expression p has type A ≡ w

What can we do about this? We can abstract over 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) with B | p | sym p
   ... | .A | _ | refl = {!!}

Perhaps error messages related to with should sometimes include the
generated code.

--
/NAD