require/typed #opaque -> contract violation

[acarrico]

As detailed in test case: https://gist.github.com/acarrico/850f9d7112104afd3e5a6dd916edf1ae

(require/typed "untyped.rkt"
  (#:opaque XPointer x-pointer?)
  (make-x (-> XPointer))
  (take-x (-> XPointer Void)))

Succeeds in Racket 6.2, fails with contract violation in 6.6, 6.7.

[AlexKnauth]

This warning is caused by my fix to #379

[acarrico]

So the All is on the predicate contract. Does that make every opaque import a violation? The value is a pointer, so, inherently unsafe. Can we get an #:unsafe-opaque import for that case?

[AlexKnauth]

Yes, specifically it's coming from the Any in a negative position in the predicate contract. Because it's in a negative position in an imported identifier (a positive position in an exported one would be the same), there is a typed value of type Any flowing into that place. Since typed racket has no way of knowing what the untyped code in the predicate will do with that value, it has to wrap it in a contract that will protect every possible thing the untyped code could do to it. However, if the value is opaque, typed racket can't safely wrap it, so it displays this warning.

As an unsafe workaround you can use unsafe-require/typed for the #:opaque version and use normal require/typed for everything else:

(unsafe-require/typed "untyped.rkt"
  [#:opaque XPointer x-pointer?])
(require/typed "untyped.rkt"
  [make-x (-> XPointer)]
  [take-x (-> XPointer Void)])

[acarrico]

I'll try that. BTW, I'm using 6.5 now, with the #:opaque. I (accidentally) introduced a cpointer tag with an _ prefix in one module and without _ prefix in another module. The #:opaque predicate caught the bug. So a little fighting with typed racket + ffi is paying off.

[acarrico]

That works in 6.7. I don't think I understand your comment, "from the Any in a negative position in the predicate contract." Why would the input of #:opaque's predicate be typed? Isn't the point of the guard to decide if the type is ok?

[AlexKnauth]

If you're importing the x-pointer? predicate into typed code and using it in typed code, you could do this:

(x-pointer? (λ ([x : Fixnum]) (+ x 1)))

The lambda there is a typed value, and without a guard there, that typed value would flow into untyped code, which could call that function. Your predicate will not do that; it will return #false instead. However, typed racket doesn't have control over that, so it has to protect it with a contract.

[acarrico]

Thanks. I understand. To avoid unsafe-require/typed, #:opaque should really create two predicates:

• one fully guarded (parameter, result), to use in fully typed code.
• one half guarded (result only) for use at the untyped->typed boundary in require/typed.

I don't know if that is actually feasible.

[AlexKnauth]

The thing is, it's not really #:opaque that's the problem; it's opaque values passed as Any. The reason it comes up with #:opaque is because of the Any in the predicate, but any other code that uses Any to pass it into untyped code will also have this problem.

However if you only have the program (take-x (make-x)), then the x-pointer is coming from untyped code, so the check on the (make-x) could be un-guarded. Then take-x doesn't need a check at all, since its argument already has the correct type. So if you never use the predicate (or any other Any stuff) you might be right.

[acarrico]

@AlexKnauth Thanks for your help with this issue. Anyone looking for an example of this usage can check out: https://github.com/acarrico/wayland-protocol/tree/master/typed/wayland-0

[AlexKnauth]

I think this still can be improved. For values coming from the untyped side, it shouldn't need to wrap it before passing the untyped value into the untyped predicate.

What I don't know is whether we would then have to wrap it after the predicate returns true, before letting it through into typed code. Right now we don't; could we still get away with not doing that if we took the wrapping away in the other place?

[acarrico]

I think that the denotation you have in mind is that Opaque values must always satisfy their predicates. The law associated with the predicate is that it should only test a static property. Unfortunately, the user could violate this law at any point, so there is no proper place to call a wrapper. With this denotation, we are always unsafe.

Instead, the denotation I have in mind is that Opaque values must satisfy their predicates when passing the untyped to typed boarder, and when cast. With this denotation, we promise less, but we are always safe.

untyped to typed border

Test the untyped value with the untyped predicate.

cast to an Opaque type

Test incoming Opaque value with the untyped predicate, fail for non-Opaque value. So an Opaque integer? can't be cast to an Integer, but it could pass the typed to untyped border, and return as a non-Opaque value.

typed to untyped border

There is nothing to do.

[acarrico]

I say we are "always safe", but is there anything you can do with an Opaque value in TR besides casting it or passing back to untyped code?

Consider make-predicate and define-predicate. To fit my denotation, these should not test if the value currently satisfies the type's #:Opaque predicate, but rather they should test if the value is Opaque and if it entered the typed world (or was cast) with that #:Opaque predicate.

[AlexKnauth]

The way cast works now is by passing it through the typed-to-untyped border and then through the untyped-to-typed border with the new type; so those 3 cases can be reduced to 2.

On the untyped to typed border, I agree that we can use the untyped predicate, and I don't think we need any-wrap/c either before or after passing it to the predicate.

On the typed to untyped border, again I agree that we don't need to use the predicate, but here I'm not sure whether or not any-wrap/c is necessary. (Edit: It is necessary)

For make-predicate, it definitely can't work in the simple way on Opaque types without introducing unsoundness, because of #457 (which was found as a sort of spin-off of this issue). Could you explain more what you mean by that?

[AlexKnauth]

I have an example of why we need any-wrap/c on the typed to untyped border. If the predicate x? always returns true, then you could take a typed value (λ ([x : Positive-Fixnum]) (- x 1)), pass it to x? (it will be wrapped inside there, but that's fine), and then once that returns true, it has the type X, and the X will not be wrapped. That's fine here though, since its still in typed code. But if you import an untyped function with the type X -> Void, it needs to be wrapped in any-wrap/c on the typed-to-untyped border.

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discourse. There might be relevant details there:

https://racket.discourse.group/t/coerce-f-and-pointer-in-typed-racket/2580/5