Typechecker should use interface's types even when specific implementation is known

[gittywithexcitement]

Steps to Reproduce

idris -p contrib Door.idr

Expected Behavior

Type checking should fail due to several errors in doorProg, but does not.

Observed Behavior

Type checking does not fail.

Details

I was attempting to write code similar to the ST tutorial but with the Door example from TDD with Idris.

This function typechecks as I expect it to. If I reorder lines (e.g. move ringBell after openDoor) then typechecking fails as expected:
doorProgPolymorphic : (DoorI m) => ST m () []

However, this function typechecks when it should not: doorProg : IO (), and the most obvious difference is that the specific implementation of the interface, IO, is known. This seems to cause typechecking to use the inferred types of the implementation functions, instead of the interface's declared types... or something like that. Note that typechecking of this function is not completely broken. For example, if unmakeDoor is commented out, the following error is given:

When checking an application of function Control.ST.>>=:
        Error in state transition: 
                Operation has preconditions: out_fn result 
                States here are: [door ::: State ()] 
                Operation has postconditions: out_fn 
                Required result states here are: \result => []

but this error should say that the state is [door ::: State (Door Open)], not State (), and this is what leads me to believe the inferred type is being typechecked, or something like that.

Complete source file:

-- Door.idr
import Control.ST

data DoorState = Open | Closed

interface DoorI (m : Type -> Type) where
  Door : DoorState -> Type
  makeDoor : ST m Var [add (Door Closed)]
  unmakeDoor : (door : Var) -> ST m () [remove door (Door Closed)]

  openDoor : (door : Var) -> ST m () [door ::: (Door Closed) :-> Door Open]
  closeDoor : (door : Var) -> ST m () [door ::: (Door Open) :-> (Door Closed)]

  ringBell : (door : Var) -> ST m () [door ::: (Door Closed)]

doorProgPolymorphic : (DoorI m) => ST m () []
doorProgPolymorphic =
  do door <- makeDoor
     ringBell door -- this would not typecheck if moved after openDoor (good)
     openDoor door
    --  openDoor door -- this does not typecheck (good)
     closeDoor door -- I had to add this to typecheck (good)
     unmakeDoor door
     pure ()

implementation DoorI IO where
  Door _ = State ()

  makeDoor = do putStrLn "making door."
                new ()
  unmakeDoor door = do delete door
                       putStrLn "unmade door."

  openDoor _ = putStrLn "creeaak"
  closeDoor _ = putStrLn "SLAM!"

  ringBell _ = putStrLn "ding dong!"

doorProg : IO ()
doorProg = run $
  do door <- makeDoor
     openDoor door
     ringBell door -- this should not typecheck because door is open
     openDoor door -- this should not typecheck because door is open
     unmakeDoor door  -- this should not typecheck because door is open
     pure ()

main : IO ()
main = doorProg

Appendix

$ idris --version
1.3.1-git:1510fce92

OS: Debian 4.17