bind for indexed monad is "wrong"

Stream: lean4

[Gary Haussmann]

I was writing up some code for an indexed monad (m i j a) and was surprised that Lean accepted my definition of an IMonad instance for it. After some tests it seems like the type of IMonad.bind is "wrong" in that it doesn't match the type I would expect. I made an #mwe using the common "you can't open a door twice" example indexed monad:

inductive DoorState where
| DoorOpen
| DoorClosed

open DoorState

-- i is "input" state and o is the "output" state
def DoorMonad (i : DoorState) (o : DoorState) (α : Type) := α

def pureDoor {α : Type} : α → DoorMonad DoorOpen DoorOpen α := id

def bindDoor : DoorMonad i₁ i₂ α → (α → DoorMonad i₂ i₃ β) → DoorMonad i₁ i₃ β := fun m f => f m

instance : Monad (DoorMonad i o) where
  pure := pureDoor
  bind := bindDoor

def startOpen : DoorMonad DoorOpen DoorOpen Unit := ()
def startClosed : DoorMonad DoorClosed DoorClosed Unit := ()
def closeDoor : α → DoorMonad DoorOpen DoorClosed α := id
def openDoor  : α → DoorMonad DoorClosed DoorOpen α := id

-- I would expect all these to have type "DoorMonad DoorOpen DoorClosed Unit"
#check bindDoor startOpen closeDoor      -- DoorMonad DoorOpen DoorClosed Unit
#check bind     startOpen closeDoor      -- DoorMonad DoorOpen DoorOpen Unit
#check          startOpen >>= closeDoor  -- DoorMonad DoorOpen DoorOpen Unit

-- correct constructions where monad input/outputs match up
#eval bindDoor (bindDoor startClosed openDoor) closeDoor
#eval bind     (bind     startClosed openDoor) closeDoor

-- these should be errors due to bad type matching (can't open a door twice in a row)
#eval bindDoor (bindDoor startClosed openDoor) openDoor     -- fails
#eval bind     (bind     startClosed openDoor) openDoor     -- no error
#eval startClosed >>= openDoor >>= openDoor                 -- no error

I'm not sure if this is a bug or if I'm incorrectly interpreting the IMonad instance. I figured that I wouldn't be able to define bind for an indexed monad at all, since the type of bindDoor isn't strictly the same as the type of bind,

[Reid Barton]

Lean can unfold the definition to see that DoorMonad i o is definitionally equal to DoorMonad i' o' for any i, o, i', o', so all these variations will type check.

[Reid Barton]

If you make DoorMonad a structure or something then you should get the behavior you expect (the Monad (DoorMonad i o) instance will be rejected).