class-field-accessor and contracts on fields

[rfindler]

TR needs to block field access to fields that aren't listed in the type when a value flows from a typed to an untyped context. Unfortunately, class-field-accessor evades the checking in this contract.

#lang racket
(require typed-racket/utils/opaque-object)

(define c%
  (class object%
    (define/public (m x) x)
    (field [f 1])
    (super-new)))

(define o
  (contract
   (object/c-opaque
    (m (-> any/c integer? integer?)))
   (new c%)
   'pos 'neg))

((class-field-accessor c% f) o) ;; => 1

It is also a problem with object/c itself:

#lang racket

(define c%
  (class object%
    (define/public (m x) x)
    (field [f 1])
    (super-new)))

(define o
  (contract
   (object/c
    (field [f none/c])
    (m (-> any/c integer? integer?)))
   (new c%)
   'pos 'neg))

((class-field-accessor c% f) o) ;; => 1

I noticed this because a new version of object/c doesn't have this bug and Color% doesn't have the s-immutable? field (but the type should) so the new version of object/c triggers a runtime error when opening the "Insert Large Letters..." dialog.

[rfindler]

(thanks @samth for helping me understand this!)

[mfelleisen]

(This looks like a failure of complete monitoring @chrdimo )

[rfindler]

Well, the contract was supposed to do this check, so I think it might reasonably be classified as a bug in object/c. The version of object/c that's here doesn't suffer from this problem.

The big worry here, in my mind, is the backwards compatibility repercussions.

[mfelleisen]

1. The question I was pushing to @chrdimo was whether the existing contract was buggy or inherently failing complete monitoring.
2. I understood that your alternative implementation of object/c fixes this, with a change of semantics and thus the injection of a backwards compatibility problem.
3. I think we should not worry about backwards compatibility here. I would much rather see a contract that corresponds to what we claim about types.

[samth]

1. This is not a failure of the theory or of the Typed Racket implementation; it's a bug in the implementation of object/c.
2. We think this will primarily have an impact on Typed Racket, because TR is the most prominent user of class contracts, particularly with restrictive contracts (the one Robby ran into rejects all field access since there's no specification).
3. Obviously we need to fix this, but equally we have to consider compatibility; we can't just break people's programs with no regard to their needs.

[rfindler]

3. I am optimistic that we can accommodate Racket's typical high backwards-compatibility standards here because we can limit ourselves to the code on the pkg server (edit: and class-field-accessors are probably not a heavily used feature) and not worry about potential code we cannot see. So my take is that we should try and find out if there is something especially difficult or not and, given any specific especially difficult situation that comes up, maybe the specifics of that situation will suggest some idea we can't possibly come up with a priori.

4. I agree with Sam here. Technically it is a change in the semantics in the sense that bug fixes are often changes in semantics but ... not really. It's a bug.

[chrdimo]

@mfelleisen If I understand correctly your question and the context of thread, I think object/c before Robby's fix was violating complete monitoring and, as a result, it was also causing TR to violate complete monitoring. I don't think there is an alternative contract that TR could generate to avoid this (without Robby's fix).

[mfelleisen]

That was my thinking at first. But let's be more precise to bring Sam and Robby onboard too:

• the existing compilation of types to contracts is broken
• choosing a different compilation to the pre-Robby-fix contract system is impossible.
• therefore complete monitoring was broken.

Robby changed the contract system so that it can discover such violations. Compiling TR's type to his revised contract system makes TR "more CM".

[samth]

@mfelleisen I don't think that's right. The existing compilation of types to contracts was correct, but there was a bug in the contract system/class system. We should think about it similarly to if the -> contract just skipped the domain contract (obviously the actual bug was less serious but it's formally similar).

[mfelleisen]

@samth Do you understand that you're in agreement with my statement?