[Agda] Simple DepType Pattern Matching

[Yuya Uezato]

Hello, Agda hackers.

I do not understand type-checking errors of the following code well and am troubled.

My Agda's version is 2.2.4

<<code>>
data Unit : Set0 where
  unit : Unit

data Ty : Unit -> Set0 where
  ty : (u : Unit) -> Ty u

{-
  why do fail type checking about "function f" ?

  Type Checker Error Message :
  u != unit of type Unit
  when checking that the pattern ty unit has type Ty unit
-}
f : Ty unit -> Unit
f (ty unit) = unit
f _         = unit
<<code>>

I think that typeof (ty unit) == Ty unit is clearness.

I write Coq version ( http://codepad.org/zPbb8qJm ) and,this passed type-checker.

I want to learn why to fail. 

Thanks for your help.

--
Yuya