Remove contract

macrotypes/type-constraints.rkt

@@ -2,6 +2,7 @@
 
 (provide add-constraints
          add-constraints/var?
+         add-constraints/variance/var?
          lookup
          lookup-Xs/keep-unsolved
          inst-type
@@ -14,6 +15,8 @@
 
 (require syntax/parse
          syntax/stx
+         syntax/id-table
+         syntax/id-set
          (for-meta -1 "typecheck.rkt")
          "stx-utils.rkt"
          )
@@ -116,6 +119,119 @@
                                      (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
                        #'a #'b)])])]))
 
+;; Variance Type Type -> Boolean
+(define (typecheck?/variance variance a b)
+  (cond
+    [(variance-covariant? variance) (typecheck? b a)]
+    [(variance-contravariant? variance) (typecheck? b a)]
+    ;; invariant and irrelevant
+    ;; TODO: use a parameter to indicate whether we're making a co/contravariant
+    ;;       typecheck?, or whether it's an invariant typecheck? (to avoid an
+    ;;       exponential cost by branching at each step)
+    [else (and (typecheck? a b)
+               (typecheck? b a))]))
+
+(define ((stx->list->c l-c) v) (and (stx-list? v) (l-c (stx->list v))))
+(define (to-datum v) (syntax->datum (datum->syntax #f v)))
+(define ((stx->datum->c d-c) v) (d-c (to-datum v)))
+(provide/contract
+ [add-constraints/variance
+  (->* {(flat-named-contract
+         "(stx-listof identifier?)"
+         (stx->list->c (listof identifier?)))
+        (free-id-table/c identifier? variance? #:immutable #t)
+        (flat-named-contract
+         "(stx-listof (stx-list/c type? type? variance?))"
+         (stx->list->c (listof (stx->list->c (list/c type? type? (stx->datum->c variance?))))))
+        (flat-named-contract
+         "(stx-listof (stx-list/c syntax? syntax?))"
+         (stx->list->c (listof (stx->list->c (list/c syntax? syntax?)))))}
+       {(free-id-table/c identifier? type? #:immutable #t)}
+       (free-id-table/c identifier? type? #:immutable #t))])
+(define (add-constraints/variance Xs X→variance ab+variance*
+                                  orig-cs
+                                  [old-solution (make-immutable-free-id-table)])
+  (define Xset (immutable-free-id-set (stx->list Xs)))
+  (define X? (curry free-id-set-member? Xset))
+  (add-constraints/variance/var? X? X→variance ab+variance* old-solution orig-cs))
+
+;; (-> Any Boolean : (∩ X Id))
+;; (ImmutableFreeIdTable (∩ X Id) Variance)
+;; (Stx-Listof (Stx-List Type Type Variance)) ;; caller-τ callee-τ variance
+;; (ImmutableFreeIdTable (∩ X Id) Type)
+;; (Stx-Listof (Stx-List Stx Stx))
+;; ->
+;; (ImmutableFreeIdTable (∩ X Id) Type)
+(define (add-constraints/variance/var? X? X→variance ab+variance* old-solution orig-cs)
+  (define-syntax-class X
+    (pattern v:id
+             #:when (X? #'v)
+             #:attr variance (or (free-id-table-ref X→variance #'a #f)
+                                 invariant)))
+  (define (do-error)
+    (define/with-syntax [(a b _) . _] ab+variance*)
+    (type-error #:src (get-orig #'b)
+                #:msg (format "couldn't unify ~~a and ~~a\n  expected: ~a\n  given: ~a"
+                              (string-join (map type->str (stx-map stx-car orig-cs)) ", ")
+                              (string-join (map type->str (stx-map stx-cadr orig-cs)) ", "))
+                (inst-type/cs/orig (free-id-table-keys old-solution)
+                                   (free-id-table-map old-solution list)
+                                   #'b
+                                   datum=?)
+                #'a))
+  (define (continue new-ab* new-solution)
+    (add-constraints/variance/var? X? X→variance new-ab* new-solution orig-cs))
+  (syntax-parse ab+variance*
+    [() old-solution]
+    [((caller-τ callee-τ:X a/b-variance) . rest)
+     ;; If a substitution was already inferred for X, check if #'a is compatible
+     (let ([existing (free-id-table-ref old-solution #'callee-τ #f)])
+       (when existing
+         (define v (variance-join (attribute callee-τ.variance)
+                                  (syntax->datum #'a/b-variance)))
+         (unless (typecheck?/variance v existing #'caller-τ)
+           (do-error))))
+     (continue #'rest
+               (free-id-table-set old-solution #'callee-τ #'caller-τ))]
+    #;[((caller callee a/b-variance) . rest)
+     #:when (displayln 'caller+callee+rest)
+     #:when (begin (display (X? #'caller))(displayln #'caller))
+     #:when (begin (display (free-identifier=? (stx-car Xs) #'callee))(displayln #'callee))
+     #:when (displayln Xs)
+     #:when (displayln #'rest)
+     #:when #f
+     #f]
+    [((caller-τ callee-τ a/b-variance) . rest)
+     ;; TODO: use this as a fallback if the "invariant" above fails?
+     #:when (typecheck?/variance (syntax->datum #'a/b-variance)
+                                 #'caller-τ
+                                 #'callee-τ)
+     (continue #'rest old-solution)]
+    [(((~Any caller-tycons caller-τᵢ ...)
+       (~Any callee-tycons callee-τᵢ ...)
+       a/b-variance)
+      . rest)
+     ;; varianceᵢ is composed with the a/b-variance. The main case of
+     ;; composition is to flip the former if the latter is contravariant,
+     ;; similarly to the xor logic operator.
+     #:with (varianceᵢ ...)
+     (for/list ([v (in-list (or (get-arg-variances #'caller-tycons)
+                                (get-arg-variances #'callee-tycons)))])
+       (variance-compose (syntax->datum #'a/b-variance) v))
+     #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(callee-τᵢ ...)))
+     #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(varianceᵢ ...)))
+     (continue #'((caller-τᵢ callee-τᵢ varianceᵢ) ... . rest)
+               old-solution)]
+    [(({~and caller (~Any caller-tycons caller-τᵢ ...)}
+       {~and callee (~Any callee-tycons callee-τᵢ ...)}
+       a/b-variance)
+      . rest)
+     #:when (= (stx-length #'(caller-τᵢ ...)) (stx-length #'(callee-τᵢ ...)))
+     (continue #`((caller-τᵢ callee-τᵢ #,invariant) ... . rest)
+               old-solution)]
+    [(_ . rest)
+     (do-error)]))
+
 (define (datum=? x y)
   (equal? (syntax->datum x) (syntax->datum y)))
 
@@ -192,6 +308,14 @@
 (define (inst-type/cs/orig Xs cs ty [var=? free-identifier=?])
   (define tys-solved (lookup-Xs/keep-unsolved Xs cs))
   (inst-type/orig tys-solved Xs ty var=?))
+;; inst-type/cs/orig/variance
+;; (ImmutableFreeIdTable X Type) Type -> Type
+(define (inst-type/cs/orig/variance solution ty [var=? free-identifier=?])
+  (define solution-as-list (free-id-table-map solution cons))
+  (inst-type/orig (map cdr solution-as-list)
+                  (map car solution-as-list)
+                  ty
+                  var=?))
 ;; inst-types/cs/orig :
 ;; (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) (Id Id -> Bool) -> (Listof Type-Stx)
 ;; the plural version of inst-type/cs/orig

turnstile/examples/mlish.rkt

@@ -2,7 +2,9 @@
 (require
  (postfix-in - racket/fixnum)
  (postfix-in - racket/flonum)
- (for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
+ (for-syntax macrotypes/type-constraints
+             macrotypes/variance-constraints
+             syntax/id-table))
 
 (extends
  "ext-stlc.rkt" 
@@ -23,6 +25,8 @@
 (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
            [tup rec] [proj get] [× ××]))
 (provide rec get ××)
+(provide (for-syntax covariant-X?
+                     contravariant-X?))
 ;; for pattern matching
 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
@@ -106,32 +110,43 @@
        #:with (~?∀ Vs expected-ty)
               (and (get-expected-type stx)
                    ((current-type-eval) (get-expected-type stx)))
+       (define Xs-variances (make-immutable-free-id-table
+                             (for/list ([X (in-syntax Xs)])
+                               (cons X (find-X-variance X tyXs)))))
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
-             (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
-             '()))
+             (add-constraints/variance Xs
+                                       Xs-variances
+                                       #`([expected-ty τ_outX #,contravariant])
+                                       ;; For error reporting only:
+                                       (list (list #'expected-ty #'τ_outX)))
+             (make-immutable-free-id-table)))
        (syntax-parse stx
          [(_ e_fn . args)
           (define-values (as- cs)
-              (for/fold ([as- null] [cs initial-cs])
-                        ([a (in-stx-list #'args)]
-                         [tyXin (in-stx-list #'(τ_inX ...))])
-                (define ty_in (inst-type/cs Xs cs tyXin))
-                (define/with-syntax [a- ty_a]
-                  (infer+erase (if (empty? (find-free-Xs Xs ty_in))
-                                   (add-expected-ty a ty_in)
-                                   a)))
-                (values 
-                 (cons #'a- as-)
-                 (add-constraints Xs cs (list (list ty_in #'ty_a))
-                                  (list (list (inst-type/cs/orig
-                                               Xs cs ty_in
-                                               (λ (id1 id2)
-                                                 (equal? (syntax->datum id1)
-                                                         (syntax->datum id2))))
-                                              #'ty_a))))))
-
-         (list (reverse as-) Xs cs)])]))
+            (for/fold ([as- null] [cs initial-cs])
+                      ([a (in-stx-list #'args)]
+                       [tyXin (in-stx-list #'(τ_inX ...))])
+              (define ty_in (inst-type/cs Xs (free-id-table-map cs list) tyXin)) ;;; TODO: is this really necessary???
+              (define/with-syntax [a- ty_a]
+                (infer+erase (if (empty? (find-free-Xs Xs ty_in))
+                                 (add-expected-ty a ty_in)
+                                 a)))
+              (values 
+               (cons #'a- as-)
+               (add-constraints/variance Xs
+                                         Xs-variances
+                                         #`([ty_a #,ty_in #,covariant])
+                                         ;; For error reporting only:
+                                         (list (list (inst-type/cs/orig
+                                                      Xs (free-id-table-map cs list) ty_in
+                                                      (λ (id1 id2)
+                                                        (equal? (syntax->datum id1)
+                                                                (syntax->datum id2))))
+                                                     #'ty_a))
+                                         ;; current cs
+                                         cs))))
+          (list (reverse as-) Xs (free-id-table-map cs list))])]))
 
   (define (mk-app-poly-infer-error stx expected-tys given-tys e_fn)
     (format (string-append

turnstile/examples/stlc+cons.rkt

@@ -14,7 +14,9 @@
          nil isnil cons list head tail
          reverse length list-ref member)
 
-(define-type-constructor List)
+(define-type-constructor List
+  #:arity = 1
+  #:arg-variances (λ (stx) (make-list (sub1 (stx-length stx)) covariant)))
 
 (define-typed-syntax nil
   [(_ ~! τi:type-ann) ≫