434569 (2) [Avatar] Offline
#1
Listing 13.1
data DoorCmd : Type  where
     Open : DoorCmd ()
     Close : DoorCmd ()
     RingBell : DoorCmd ()
     Pure : ty -> DoorCmd ty
     (>>=) : DoorCmd a -> (a -> DoorCmd b) -> DoorCmd b

does not type check with the error
When checking type of Open:
Too many arguments for Main.DoorCmd


Changing the definition to
data DoorCmd : Type -> Type where
makes the the listing type check again.