failing idris program

console.log

Rolands-MBP:idris-test rkuhn$ idris test.idr -o test
idris: Can't happen pickAlt - impossible case found
CallStack (from HasCallStack):
  error, called at src/IRTS/LangOpts.hs:248:25 in idris-1.3.2-9ZZwhBKx1W3Fg3FkIorcnE:IRTS.LangOpts

test.idr

module Main

data DoorState = Closed | Opened
data Command = Open | Close

Show DoorState where
  show Closed = "Closed"
  show Opened = "Opened"

data Jar : Maybe DoorState -> Type where
  AJar : (d: DoorState) -> Jar (Just d)
  NoJar : Jar Nothing

Show (Jar d) where
  show (AJar d) = show d
  show NoJar = "nothing"

total machine : DoorState -> Command -> Type
machine Closed Open = Jar $ Just Opened
machine Opened Close = Jar $ Just Closed
machine Closed Close = Jar Nothing
machine Opened Open = Jar Nothing

total f: (d: DoorState) -> (c: Command) -> machine d c
f Closed Open = AJar Opened
f Opened Close = AJar Closed
f Closed Close = NoJar
f Opened Open = NoJar

main : IO ()
main = printLn $ f Opened Open