[Agda] a bug in the type checker?

[David Leduc]

Hi,

In the definition of  t  below, the type checker does not see that
[ t ]  is equal to  unit  and thus raise an error.
I believe it is a bug, isnt it?
Is there a temporary workaround until this bug is fixed?

Note that I am using the development version of Agda.
The same problem occurs even if I remove the coinduction stuff.

module test where

open import Coinduction

data unit : Set where
  tt : unit

mutual
  data T : Set1 where
    makeT : (A : Set) -> (t : ∞ T) -> [ ♭ t ] -> T

  [_] : (t : T) -> Set
  [ makeT A _ _ ] = A

t : T
t = makeT unit (♯ t) tt