The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

434569 (2) [Avatar] Offline
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.