[Agda] Is this a bug?

[Sivaram Gowkanapalli]

Hello,

Just wondering if this is a bug.

agda --version
Agda version 2.2.11

-- agda code below


module test where

data Bool : Set where
   true  : Bool
   false : Bool

data ℕ : Set where
   zero : ℕ
   succ : ℕ → ℕ

data Type : (A : Set) → Set where
   isBool : Type Bool
   isℕ    : Type ℕ

g : {A : Set} → Type A → Type A → ℕ
g (isBool) (isBool) = zero
g (isℕ) (isℕ) = (succ zero)


-- agda error message below:

/home/j/dev/apps/haskell/agda/learn/test.agda:17,1-18,28
Cannot split on the constructor isℕ
when checking the definition of g

Any thoughts, please?

Thanks
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110503/dafe1569/attachment.html