[evincarofautumn]

Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode:

    // open : string -> file_mode -> (f : file) | f @ read * f @ close
    f = open "input.dat" Read

    // close : (f : file) | f @ read * f @ close -> ()
    close f

    // getline : (f : file) | f @ read -> string | f @ read
    s = getline f

“open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.