Add sealing contracts for row polymorphic types

This enables contract generation in the negative
direction (untyped->typed) for row polymorphic types
(basically mixin types).

Depends on `class-seal` and `class-unseal` in
the racket/class library.

typed-racket-lib/typed-racket/env/row-constraint-env.rkt

@@ -39,7 +39,8 @@
 ;; lookup-row-constraints : Symbol -> RowConstraint
 ;; returns the mapped-to constraints or #f
 (define (lookup-row-constraints var)
-  (cdr (assq var (current-row-constraints))))
+  (define result (assq var (current-row-constraints)))
+  (and result (cdr result)))
 
 ;; extend : Env Symbol RowConstraint -> Env
 ;; extend type environment with a var-constraints pair

typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -147,6 +147,7 @@
       typed-racket/utils/any-wrap typed-racket/utils/struct-type-c
       typed-racket/utils/opaque-object
       typed-racket/utils/evt-contract
+      typed-racket/utils/sealing-contract
       unstable/contract racket/contract/parametric))
 
 ;; Should the above requires be included in the output?
@@ -472,28 +473,46 @@
          ;; we need to generate absent clauses for non-opaque class contracts
          ;; that occur inside of a mixin type
          (define absents
-           (cond [(F? row-var)
-                  (define constraints (lookup-row-constraints (F-n row-var)))
-                  ;; the constraints with no corresponding type/contract need
-                  ;; to be absent
-                  (append (remove* field-names (cadr constraints))
-                          (remove* public-names (caddr constraints)))]
+           (cond [;; row constraints are only mapped when it's a row polymorphic
+                  ;; function in *positive* position (with no sealing)
+                  (and (F? row-var) (lookup-row-constraints (F-n row-var)))
+                  =>
+                  (λ (constraints)
+                    ;; the constraints with no corresponding type/contract need
+                    ;; to be absent
+                    (append (remove* field-names (cadr constraints))
+                            (remove* public-names (caddr constraints))))]
                  [else null]))
-         (class/sc ;; only enforce opaqueness if there's no row variable
-                   ;; and we are importing from untyped
-                   (and (from-untyped? typed-side) (not row-var))
-                   (append
-                     (map (λ (n sc) (member-spec 'override n sc))
-                          override-names (map t->sc/meth override-types))
-                     (map (λ (n sc) (member-spec 'pubment n sc))
-                          pubment-names (map t->sc/meth pubment-types))
-                     (map (λ (n sc) (member-spec 'inner n sc))
-                          augment-names (map t->sc/meth augment-types))
-                     (map (λ (n sc) (member-spec 'init n sc))
-                          init-names (map t->sc/neg init-types))
-                     (map (λ (n sc) (member-spec 'field n sc))
-                          field-names (map t->sc/both field-types)))
-                   absents)]
+         ;; add a seal/unseal if there was a row variable and the
+         ;; row polymorphic function type was in negative position
+         (define seal/sc
+           (and (F? row-var)
+                (not (lookup-row-constraints (F-n row-var)))
+                (triple-lookup
+                 (hash-ref recursive-values (F-n row-var)
+                           (λ () (error 'type->static-contract
+                                        "Recursive value lookup failed. ~a ~a"
+                                        recursive-values (F-n row-var))))
+                 typed-side)))
+         (define sc-for-class
+           (class/sc ;; only enforce opaqueness if there's no row variable
+                     ;; and we are importing from untyped
+                     (and (from-untyped? typed-side) (not row-var))
+                     (append
+                       (map (λ (n sc) (member-spec 'override n sc))
+                            override-names (map t->sc/meth override-types))
+                       (map (λ (n sc) (member-spec 'pubment n sc))
+                            pubment-names (map t->sc/meth pubment-types))
+                       (map (λ (n sc) (member-spec 'inner n sc))
+                            augment-names (map t->sc/meth augment-types))
+                       (map (λ (n sc) (member-spec 'init n sc))
+                            init-names (map t->sc/neg init-types))
+                       (map (λ (n sc) (member-spec 'field n sc))
+                            field-names (map t->sc/both field-types)))
+                     absents))
+         (if seal/sc
+             (and/sc seal/sc sc-for-class)
+             sc-for-class)]
         [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
          (cond
            [(dict-ref recursive-values nm #f)]
@@ -695,8 +714,29 @@
                                 (hash-set rv v (same any/sc)))))
         (extend-row-constraints vs (list constraints)
           (t->sc body #:recursive-values recursive-values)))
-      ;; FIXME: needs sealing contracts, disabled for now
-      (fail #:reason "cannot generate contract for row polymorphic type")))
+      (match-let ([(PolyRow-names: vs-nm constraints b) type])
+        ;; FIXME: abstract this
+        (define function-type?
+          (let loop ([ty b])
+            (match (resolve ty)
+              [(Function: _) #t]
+              [(Union: elems) (andmap loop elems)]
+              [(Poly: _ body) (loop body)]
+              [(PolyDots: _ body) (loop body)]
+              [_ #f])))
+        (unless function-type?
+          (fail #:reason "cannot generate contract for non-function polymorphic type"))
+        (let ([temporaries (generate-temporaries vs-nm)])
+          (define rv (for/fold ([rv recursive-values])
+                               ([temp temporaries]
+                                [v-nm vs-nm])
+                       (hash-set rv v-nm (same (sealing-var/sc temp)))))
+          (parameterize ([bound-names (append (bound-names) vs-nm)])
+            ;; Only the first three sets of constraints seem to be needed
+            ;; since augment clauses don't make sense without a corresponding
+            ;; public method too. This invariant has to be enforced though.
+            (sealing->/sc temporaries (take constraints 3)
+              (t->sc b #:recursive-values rv)))))))
 
 ;; Predicate that checks for an App type with a recursive
 ;; Name type in application position

typed-racket-lib/typed-racket/static-contracts/combinators/parametric.rkt

@@ -1,6 +1,6 @@
 #lang racket/base
 
-;; Static contract for parametric->/c.
+;; Static contract for parametric->/c and sealing->/sc.
 
 (require
   "../structures.rkt"
@@ -8,17 +8,25 @@
   "../terminal.rkt"
   racket/match
   racket/contract
-  (for-template racket/base racket/contract/parametric)
+  (for-template racket/base racket/contract/parametric
+                typed-racket/utils/sealing-contract)
   (for-syntax racket/base syntax/parse))
 
 (provide
   (contract-out
     [parametric->/sc ((listof identifier?) static-contract? . -> . static-contract?)]
-    [parametric-var/sc (identifier? . -> . static-contract?)])
+    [parametric-var/sc (identifier? . -> . static-contract?)]
+    [sealing->/sc ((listof identifier?)
+                   (list/c (listof symbol?) (listof symbol?) (listof symbol?))
+                   static-contract? . -> . static-contract?)]
+    [sealing-var/sc (identifier? . -> . static-contract?)])
   parametric->/sc:
+  sealing->/sc:
   (rename-out
     [parametric-var/sc parametric-var/sc:]
-    [parametric-combinator? parametric->/sc?]))
+    [parametric-combinator? parametric->/sc?]
+    [sealing-var/sc sealing-var/sc:]
+    [sealing-combinator? sealing->/sc?]))
 
 
 (struct parametric-combinator combinator (vars)
@@ -54,3 +62,38 @@
 (define-terminal-sc parametric-var/sc (id) #:impersonator
   #:printer (v p mode) (display (syntax-e (parametric-var/sc-id v)) p)
    id)
+
+;; combinator for sealing-> contracts for row polymorphism
+(struct sealing-combinator combinator (vars members)
+  #:transparent
+  #:property prop:combinator-name "sealing->/sc"
+  #:methods gen:sc
+    [(define (sc-map v f)
+       (match v
+        [(sealing-combinator (list arg) vars members)
+         (sealing-combinator (list (f arg 'covariant)) vars members)]))
+     (define (sc-traverse v f)
+       (match v
+        [(sealing-combinator (list arg) vars members)
+         (f arg 'covariant)
+         (void)]))
+     (define (sc->contract v f)
+       (match v
+        [(sealing-combinator (list arg) vars members)
+         #`(sealing->/c #,(car vars) #,members #,(f arg))]))
+     (define (sc->constraints v f)
+       (match v
+        [(sealing-combinator (list arg) vars members)
+         (merge-restricts* 'impersonator  (list (f arg)))]))])
+
+(define (sealing->/sc vars members body)
+  (sealing-combinator (list body) vars members))
+
+(define-match-expander sealing->/sc:
+  (syntax-parser
+    [(_ vars members body)
+     #'(sealing-combinator (list body) vars members)]))
+
+(define-terminal-sc sealing-var/sc (id) #:impersonator
+  #:printer (v p mode) (display (syntax-e (sealing-var/sc-id v)) p)
+   id)

typed-racket-lib/typed-racket/static-contracts/instantiate.rkt

@@ -99,8 +99,10 @@
   (define (recur sc)
     (cond [(and cache (hash-ref cache sc #f)) => car]
           [(arr/sc? sc) (make-contract sc)]
-          [(parametric->/sc? sc)
-           (match-define (parametric->/sc: vars _) sc)
+          [(or (parametric->/sc? sc) (sealing->/sc? sc))
+           (match-define (or (parametric->/sc: vars _)
+                             (sealing->/sc: vars _ _))
+                         sc)
            (parameterize ([bound-names (append vars (bound-names))])
              (make-contract sc))]
           ;; If any names are bound, the contract can't be shared
@@ -167,6 +169,7 @@
     (define/match (free? sc _)
       [((or (recursive-sc-use name*)
             (parametric-var/sc: name*)
+            (sealing-var/sc: name*)
             (name/sc: name*))
         _)
        (when (free-identifier=? name name*)

typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt

@@ -41,7 +41,7 @@
        (add-equation! eqs (get-var sc)
                       (lambda () (for/sum ((e elems))
                                    (variable-ref (get-var e)))))]
-      [(parametric-var/sc: id)
+      [(or (parametric-var/sc: id) (sealing-var/sc: id))
        (add-equation! eqs (get-var sc) (lambda () 1))]
       [(recursive-sc names values body)
        (for ([name names] [value values])

typed-racket-lib/typed-racket/utils/sealing-contract.rkt

@@ -0,0 +1,127 @@
+#lang racket/base
+
+;; This module provides a sealing->/c which operates like the parametric->/c
+;; contract except for classes and with partial sealing instead of fully
+;; opaque sealing.
+
+(require racket/class
+         racket/contract
+         racket/match
+         (for-syntax racket/base
+                     syntax/parse))
+
+(provide sealing->/c)
+
+(define-syntax (sealing->/c stx)
+  (syntax-parse stx
+    [(_ ?var:id [(?i:id ...) (?f:id ...) (?m:id ...)] ?c)
+     #`(sealing-contract (quote #,(syntax->datum stx))
+                         (quote ((?i ...) (?f ...) (?m ...)))
+                         (λ (?var) ?c))]))
+
+;; represents a sealing function contract
+;; name     - a datum for the printed form of the contract
+;; unsealed - init/field/method names left unsealed by sealers/unsealers
+;; proc     - a procedure that constructs the whole contract
+(struct sealing-contract (name unsealed proc)
+        #:property prop:contract
+        (build-contract-property
+         #:name (λ (ctc) (sealing-contract-name ctc))
+         #:stronger
+         (λ (this that)
+           (cond
+            [(sealing-contract? that)
+             (define this-unsealed (sealing-contract-unsealed this))
+             (define that-unsealed (sealing-contract-unsealed that))
+             (match-define (list this-inits this-fields this-methods) this-unsealed)
+             (match-define (list that-inits that-fields that-methods) that-unsealed)
+             (define (that-subset-of-this? this that)
+               (for/and ([that-member (in-list that)])
+                 (member that-member this)))
+             (that-subset-of-this? this-inits that-inits)
+             (that-subset-of-this? this-fields that-fields)
+             (that-subset-of-this? this-methods that-methods)
+             (cond [that-subset-of-this?
+                    (define sealer/unsealer
+                      (seal/unseal (gensym) #t that-unsealed))
+                    ;; see if the instantiated contract is stronger
+                    (contract-stronger? ((sealing-contract-proc this)
+                                         sealer/unsealer)
+                                        ((sealing-contract-proc that)
+                                         sealer/unsealer))]
+                   [else #f])]
+            [else #f]))
+         #:projection
+         (λ (ctc)
+           (define unsealed (sealing-contract-unsealed ctc))
+           (define body (sealing-contract-proc ctc))
+           (λ (blame)
+             (define negative? (blame-swapped? blame))
+             (define (make-seal-function orig-fun)
+               (define sealing-key (gensym))
+               (define sealer/unsealer
+                 (seal/unseal sealing-key negative? unsealed))
+               (define body-proj
+                 (contract-projection (body sealer/unsealer)))
+               ((body-proj blame) orig-fun))
+             (λ (val)
+               (unless (procedure? val)
+                 (raise-blame-error
+                  blame val
+                  '(expected "a procedure" given: "~e") val))
+               ;; ok to return an unrelated function since this
+               ;; is an impersonator contract
+               (make-keyword-procedure (λ (kws kw-args . rst)
+                                         (keyword-apply (make-seal-function val)
+                                                        kws kw-args rst))))))))
+
+;; represents a contract for each polymorphic seal/unseal corresponding
+;; to a variable
+;; key       - a fresh symbol used as a key
+;; positive? - whether the contract starts in positive/negative
+;; unsealed - names that are to be unsealed by sealers/unsealers
+(struct seal/unseal (key positive? unsealed)
+        #:property prop:contract
+        (build-contract-property
+         #:name (λ (ctc)
+                  (if positive?
+                      `(seal/c ,(seal/unseal-key ctc)
+                               ,(seal/unseal-unsealed ctc))
+                      '(unseal/c ,(seal/unseal-key ctc))))
+         #:stronger (λ (this that) (eq? this that))
+         #:projection
+         (λ (ctc)
+           (define sealing-key (seal/unseal-key ctc))
+           (define unsealed (seal/unseal-unsealed ctc))
+           (λ (blame)
+             (λ (val)
+               (unless (class? val)
+                 (raise-blame-error
+                  blame val
+                  '(expected: "a class" given: "~e") val))
+               (match-define (list init field method) unsealed)
+               (if (equal? (blame-original? blame)
+                           (seal/unseal-positive? ctc))
+                   (class-seal val sealing-key init field method
+                               (inst-err val blame)
+                               (subclass-err val blame))
+                   (class-unseal val sealing-key
+                                 (unseal-err val blame))))))))
+
+;; error functions for use with class-seal, class-unseal
+(define ((inst-err val blame) cls)
+  (raise-blame-error
+   blame val
+   "cannot instantiated a row polymorphic class"))
+
+(define ((subclass-err val blame) cls names)
+  (raise-blame-error
+   blame val
+   "cannot subclass a row polymorphic class with disallowed members ~a"
+   names))
+
+(define ((unseal-err val blame) cls)
+  (raise-blame-error
+   blame val
+   '(expected "matching row polymorphic class"
+     given: "an unrelated class")))

typed-racket-test/fail/sealing-contract-1.rkt

@@ -0,0 +1,24 @@
+#;
+(exn-pred #rx"an unrelated class")
+#lang racket/base
+
+(module u racket
+  ;; drops cls on the floor, doesn't match spec
+  (define (mixin cls)
+    (class object% (super-new)))
+
+  (provide mixin))
+
+(module t typed/racket
+  ;; expects a mixin that adds n
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r [n (-> Integer Integer)])))])
+
+  (mixin (class object%
+           (super-new)
+           (define/public (m x) x))))
+
+(require 't)

typed-racket-test/fail/sealing-contract-2.rkt

@@ -0,0 +1,26 @@
+#;
+(exn-pred #rx"disallowed members \\(m\\)")
+#lang racket/base
+
+(module u racket
+  ;; adds m instead of n like the spec says
+  (define (mixin cls)
+    (class cls
+      (super-new)
+      (define/public (m x) x)))
+
+  (provide mixin))
+
+(module t typed/racket
+  ;; expects a mixin that adds n
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r [n (-> Integer Integer)])))])
+
+  (mixin (class object%
+           (super-new)
+           (define/public (m x) x))))
+
+(require 't)

typed-racket-test/fail/sealing-contract-3.rkt

@@ -0,0 +1,26 @@
+#;
+(exn-pred #rx"disallowed members \\(f\\)")
+#lang racket/base
+
+(module u racket
+  ;; adds f instead of g like the spec says
+  (define (mixin cls)
+    (class cls
+      (super-new)
+      (field [f 0])))
+
+  (provide mixin))
+
+(module t typed/racket
+  ;; expects a mixin that adds g
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r (field [g Integer]))))])
+
+  (mixin (class object%
+           (super-new)
+           (field [f 1]))))
+
+(require 't)

typed-racket-test/fail/sealing-contract-4.rkt

@@ -0,0 +1,35 @@
+#;
+(exn-pred #rx"unrelated class")
+#lang racket/base
+
+(module u racket
+  (define state #f)
+
+  ;; don't allow smuggling with mutation either
+  (define (mixin cls)
+    (define result
+      (if (not state)
+          (class cls
+            (super-new)
+            (define/public (n x) x))
+          ;; should subclass from cls, not state since otherwise
+          ;; we lose the `m` method
+          (class state (super-new))))
+    (set! state cls)
+    result)
+
+  (provide mixin))
+
+(module t typed/racket
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r [n (-> Integer Integer)])))])
+
+  (mixin (class object% (super-new)))
+  (mixin (class object%
+           (super-new)
+           (define/public (m x) x))))
+
+(require 't)

typed-racket-test/succeed/sealing-contract-1.rkt

@@ -0,0 +1,23 @@
+#lang racket/base
+
+(module u racket
+  (define (mixin cls)
+    (class cls
+      (super-new)
+      (define/public (n x) (add1 x))))
+
+  (provide mixin))
+
+(module t typed/racket
+  ;; expects a mixin that adds n
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r [n (-> Integer Integer)])))])
+
+  (mixin (class object%
+           (super-new)
+           (define/public (m x) x))))
+
+(require 't)

typed-racket-test/succeed/sealing-contract-2.rkt

@@ -0,0 +1,23 @@
+#lang racket/base
+
+(module u racket
+  (define (mixin cls)
+    (class cls
+      (super-new)
+      (field [g 0])))
+
+  (provide mixin))
+
+(module t typed/racket
+  ;; expects a mixin that adds g
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r (field [g Integer]))))])
+
+  (mixin (class object%
+           (super-new)
+           (field [f 1]))))
+
+(require 't)

typed-racket-test/succeed/sealing-contract-3.rkt

@@ -0,0 +1,26 @@
+#lang racket/base
+
+(module u racket
+  (define state #f)
+
+  (define (mixin cls)
+    (class cls
+      (super-new)
+      (define/public (n x) x)))
+
+  (provide mixin))
+
+(module t typed/racket
+  (require/typed (submod ".." u)
+                 [mixin
+                  (All (r #:row)
+                   (-> (Class #:row-var r)
+                       (Class #:row-var r [n (-> Integer Integer)])))])
+
+  ;; ok to call mixin with different types
+  (mixin (class object% (super-new)))
+  (mixin (class object%
+           (super-new)
+           (define/public (m x) x))))
+
+(require 't)