Is it possible to make Mutable Types support subtype?

[NoahStoryM]

I tried to write mlength for mlist, but it can't work for (MPairof Natural Null) type:

(: mlength (-> (MListof Natural) Natural))
(define mlength
  (λ (m)
    (if (null? m)
        0
        (add1 (mlength (mcdr m))))))

(: mls (MPairof Natural Null))
(define mls (mcons 9 '()))


(mlength mls)

I can understand it: (MPairof Natural Null) is not subtype of (MListof Natural)
because we can't run (set-mcdr! mls (ann (mcons 8 '()) (MListof Natural))).
But it's legal for mlength to run (set-mcdr! m (ann (mcons 8 '()) (MListof Natural)))
in its body when mls bound to m, which cause conflict.

I wonder if it's possible to make Mutable Types support subtype, and when TR
found conflict, just throw an exception?
(I haven't studied type theory, I just wonder if it's feasible?)

for example:

(: mls (MListof Natural))
(define mls (mcons 9 '()))

(: change-1st! (-> (MListof Any) #:immediately Void))
(define change-1st!
  (λ (mls)
    (unless (null? mls)
      (set-mcar! mls 'sym))))

(displayln mls)
(change-1st! mls)
(displayln mls)

when apply mls to change-1st!, it will record mls's type and value.
If mls's type is changed, then TR throws an exception.
(typecheck happens when the Mutable Type's assign operator was applied if the keyword is #:immediately,
or it happens when the calculation is finished if the keyword is #:end,
or it doesn't happen if the keyword is #:never)

[samth]

This is a possible language design -- it's roughly how the array type in Java works. When you create an array in Java, it records the type it's supposed to have, and if you try to assign something wrong to it then there's a runtime error. So we could have a design where mutable pairs recorded the types of their two fields when they were created, and did runtime checks for those types on assignment. Then we would have covariant subtyping on mutable pairs.

Unfortunately, this is a very different design than what Racket has today, so it would make it impossible for mpairs in Typed Racket to be the same as mpairs in Racket. That's a reasonable choice for a language, but Typed Racket aims to be highly-compatibly with Racket, so it won't work for Typed Racket.

I'm going to move this to a "discussion" because that seems like a better place for discussing possible options for programs like this.