trying-to-understand-multiplicity-idris.md

original

data DoorState = Open | Closed

data Door : DoorState -> Type where
     MkDoor : (doorId : Int) -> Door st

openDoor : (1 d : Door Closed) -> Door Open

closeDoor : (1 d : Door Open) -> Door Closed

newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()

deleteDoor : (1 d : Door Closed) -> IO ()


doorProg : IO ()
doorProg
    = newDoor $ \d => do
          let d' = openDoor d
              d'' = closeDoor d'
          deleteDoor d''

---

idris2 --check ./doorProg.idr

Error: While processing right hand side of doorProg. There are 2 uses of linear name d'.

./doorProg.idr:17:15--17:30
    |
 17 |           let d' = openDoor d
    |               ^^^^^^^^^^^^^^^

Suggestion: linearly bounded variables must be used exactly once.

data DoorState = Open | Closed

data Door : DoorState -> Type where
     MkDoor : (doorId : Int) -> Door st

openDoor : (1 d : Door Closed) -> Door Open

closeDoor : (1 d : Door Open) -> Door Closed

newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()

deleteDoor : (1 d : Door Open) -> (1 d : Door Closed) -> IO ()

doorProg : IO ()
doorProg
    = newDoor $ \d => do
          let d' = openDoor d
              d'' = closeDoor d'
          deleteDoor d' d''

---

compiles as expected

data DoorState = Open | Closed

data Door : DoorState -> Type where
     MkDoor : (doorId : Int) -> Door st

openDoor : (1 d : Door Closed) -> Door Open

closeDoor : (1 d : Door Open) -> Door Closed

newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()

deleteDoor : (0 d : Door Open) -> (1 d : Door Closed) -> IO ()

doorProg : IO ()
doorProg
    = newDoor $ \d => do
          let d' = openDoor d
              d'' = closeDoor d'
          deleteDoor d' d''