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

[David Leduc]

Hi,

Why the function "test" below is rejected by the type-checker?
I have the same error message with "test'" where
I have translated the rewrite clause into a "with" clause.
How can I convince Agda that it is well-typed?
Note that it type checks if I replace "sym p" with "p".


{-# 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 = {!!}