infer variances for recursive and mutually recursive datatypes

tapl/mlish.rkt

@@ -1,5 +1,5 @@
 #lang s-exp "typecheck.rkt"
-(require racket/fixnum racket/flonum)
+(require racket/fixnum racket/flonum (for-syntax "variance-constraints.rkt"))
 
 (extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
           #:rename [~→ ~ext-stlc:→])
@@ -310,21 +310,76 @@
        (make-list (length Xs) irrelevant)]
       [_ (make-list (length Xs) invariant)]))
 
-  ;; infer-variances : Id (Stx-Listof Id) (Stx-Listof Type-Stx) -> (Listof Variance)
-  (define (infer-variances type-constructor Xs τs)
-    (define expanded-tys
-      (for/list ([τ (in-list (stx->list τs))])
-        (with-handlers ([exn:fail:syntax? (λ (e) #false)])
-          ((current-type-eval) #`(∀ #,Xs #,τ)))))
-    (for/fold ([acc (make-list (length (stx->list Xs)) irrelevant)])
-              ([ty (in-list expanded-tys)])
-      (cond [ty
-             (define/syntax-parse (~?∀ Xs τ) ty)
-             (map variance-join
-                  acc
-                  (find-variances (syntax->list #'Xs) #'τ covariant))]
-            [else
-             (make-list (length acc) invariant)])))
+  ;; find-variances/exprs : (Listof Id) Type [Variance-Expr] -> (Listof Variance-Expr)
+  ;; Like find-variances, but works with Variance-Exprs instead of
+  ;; concrete variance values.
+  (define (find-variances/exprs Xs ty [ctxt-variance covariant])
+    (syntax-parse ty
+      [A:id
+       (for/list ([X (in-list Xs)])
+         (cond [(free-identifier=? X #'A) ctxt-variance]
+               [else irrelevant]))]
+      [(~Any tycons)
+       (make-list (length Xs) irrelevant)]
+      [(~?∀ () (~Any tycons τ ...))
+       #:when (get-arg-variances #'tycons)
+       #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
+       (define τ-ctxt-variances
+         (for/list ([arg-variance (in-list (get-arg-variances #'tycons))])
+           (variance-compose/expr ctxt-variance arg-variance)))
+       (for/fold ([acc (make-list (length Xs) irrelevant)])
+                 ([τ (in-list (syntax->list #'[τ ...]))]
+                  [τ-ctxt-variance (in-list τ-ctxt-variances)])
+         (map variance-join/expr
+              acc
+              (find-variances/exprs Xs τ τ-ctxt-variance)))]
+      [ty
+       #:when (not (for/or ([X (in-list Xs)])
+                     (stx-contains-id? #'ty X)))
+       (make-list (length Xs) irrelevant)]
+      [_ (make-list (length Xs) invariant)]))
+
+  ;; current-variance-constraints : (U False (Mutable-Setof Variance-Constraint))
+  ;; If this is false, that means that infer-variances should return concrete Variance values.
+  ;; If it's a mutable set, that means that infer-variances should mutate it and return false,
+  ;; and type constructors should return the list of variance vars.
+  (define current-variance-constraints (make-parameter #false))
+
+  ;; infer-variances :
+  ;; ((-> Stx) -> Stx) (Listof Variance-Var) (Listof Id) (Listof Type-Stx)
+  ;; -> (U False (Listof Variance))
+  (define (infer-variances with-variance-vars-okay variance-vars Xs τs)
+    (cond
+      [(current-variance-constraints)
+       (define variance-constraints (current-variance-constraints))
+       (define variance-exprs
+         (for/fold ([exprs (make-list (length variance-vars) irrelevant)])
+                   ([τ (in-list τs)])
+           (define/syntax-parse (~?∀ Xs* τ*)
+             ;; This can mutate variance-constraints!
+             ;; This avoids causing an infinite loop by having the type
+             ;; constructors provide with-variance-vars-okay so that within
+             ;; this call they declare variance-vars for their variances.
+             (with-variance-vars-okay
+              (λ () ((current-type-eval) #`(∀ #,Xs #,τ)))))
+           (map variance-join/expr
+                exprs
+                (find-variances/exprs (syntax->list #'Xs*) #'τ* covariant))))
+       (for ([var (in-list variance-vars)]
+             [expr (in-list variance-exprs)])
+         (set-add! variance-constraints (variance= var expr)))
+       #f]
+      [else
+       (define variance-constraints (mutable-set))
+       ;; This will mutate variance-constraints!
+       (parameterize ([current-variance-constraints variance-constraints])
+         (infer-variances with-variance-vars-okay variance-vars Xs τs))
+       (define mapping
+         (solve-variance-constraints variance-vars
+                                     (set->list variance-constraints)
+                                     (variance-mapping)))
+       (for/list ([var (in-list variance-vars)])
+         (variance-mapping-ref mapping var))]))
 
   ;; compute unbound tyvars in one unexpanded type ty
   (define (compute-tyvar1 ty)
@@ -460,15 +515,47 @@
                                      #'(StructName ...) #'((fld ...) ...))
      #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
      #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
-     #:with [arg-variance ...]
-     (infer-variances #'Name #'[X ...] #'[τ ... ...])
      #`(begin
          (define-syntax (NameExtraInfo stx)
            (syntax-parse stx
              [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
+         (begin-for-syntax
+           ;; arg-variance-vars : (List Variance-Var ...)
+           (define arg-variance-vars
+             (list (variance-var (syntax-e (generate-temporary 'X))) ...))
+           ;; variance-vars-okay? : (Parameterof Boolean)
+           ;; A parameter that determines whether or not it's okay for
+           ;; this type constructor to return a list of Variance-Vars
+           ;; for the variances.
+           (define variance-vars-okay? (make-parameter #false))
+           ;; with-variance-vars-okay : (-> A) -> A
+           (define (with-variance-vars-okay f)
+             (parameterize ([variance-vars-okay? #true])
+               (f)))
+           ;; arg-variances : (Boxof (U False (List Variance ...)))
+           ;; If false, means that the arg variances have not been
+           ;; computed yet. Otherwise, stores the complete computed
+           ;; variances for the arguments to this type constructor.
+           (define arg-variances (box #f)))
          (define-type-constructor Name
            #:arity = #,(stx-length #'(X ...))
-           #:arg-variances (λ (stx) (list 'arg-variance ...))
+           #:arg-variances (λ (stx)
+                             (or (unbox arg-variances)
+                                 (cond
+                                   [(variance-vars-okay?)
+                                    arg-variance-vars]
+                                   [else
+                                    (define inferred-variances
+                                      (infer-variances
+                                       with-variance-vars-okay
+                                       arg-variance-vars
+                                       (list #'X ...)
+                                       (list #'τ ... ...)))
+                                    (cond [inferred-variances
+                                           (set-box! arg-variances inferred-variances)
+                                           inferred-variances]
+                                          [else
+                                           arg-variance-vars])])))
            #:extra-info 'NameExtraInfo
            #:no-provide)
          (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...

tapl/tests/mlish/infer-variances.mlish

@@ -0,0 +1,243 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define-type T1 t1)
+;; No type arguments to determine variance for.
+
+(check-type t1 : T1 -> t1)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Non-Recursive Types
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T2 X) t2)
+;; X should be inferred to be irrelevant within (T2 X).
+;; That means it should be both covariant and contravariant.
+
+;; This checks that X is covariant within (T2 X).
+(define (t2* → (T2 X)) t2)
+(define (t2** → (→ (T2 X))) t2*)
+(check-type (t2**) : (→/test (T2 X)))
+
+;; This checks that X is contravariant within (T2 X),
+;; by checking that X is covariant within (→ (T2 X) Int).
+(define (t2->int [t2 : (T2 X)] → Int) 0)
+(define (t2->int* → (→ (T2 X) Int)) t2->int)
+(check-type (t2->int*) : (→/test (T2 X) Int))
+
+;; This checks that X is irrelevant, even within a Ref type,
+;; by checking that X is covariant within (Ref (T2 X)).
+;; This is still sound because a value of type (Ref (T2 X)) will never
+;; contain anything of type X anyway. X is irrelevant within it.
+(define (ref-t2* → (Ref (T2 X))) (ref (t2 {X})))
+(define (ref-t2** → (→ (Ref (T2 X)))) ref-t2*)
+(check-type (ref-t2**) : (→/test (Ref (T2 X))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T3 X) t3-none (t3-some X))
+;; X should be inferred to be covariant within (T3 X).
+
+;; This checks that X is covariant within (T3 X).
+(define (t3-none* → (T3 X)) t3-none)
+(define (t3-none** → (→ (T3 X))) t3-none*)
+(check-type (t3-none**) : (→/test (T3 X)))
+
+;; This checks that X is not contravariant within (T3 X),
+;; by checking that X is not covariant within (→ (T3 X) Int).
+(define (t3->int [t3 : (T3 X)] → Int) 0)
+(define (t3->int* → (→ (T3 X) Int)) t3->int)
+(typecheck-fail (t3->int*))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T4 X) t4-none (t4-some (→ X Int)))
+;; X should be inferred to be contravariant within (T4 X).
+
+;; This checks that X is not covariant within (T4 X).
+(define (t4-none* → (T4 X)) t4-none)
+(define (t4-none** → (→ (T4 X))) t4-none*)
+(typecheck-fail (t4-none**))
+
+;; This checks that X is contravariant within (T4 X),
+;; by checking that X is covariant within (→ (T4 X) Int).
+(define (t4->int [t4 : (T4 X)] → Int) 0)
+(define (t4->int* → (→ (T4 X) Int)) t4->int)
+(check-type (t4->int*) : (→/test (T4 X) Int))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T5 X) t5-none (t5-some+ X) (t5-some- (→ X Int)))
+;; X should be inferred to be invariant within (T5 X).
+
+;; This checks that X is not covariant within (T5 X).
+(define (t5-none* → (T5 X)) t5-none)
+(define (t5-none** → (→ (T5 X))) t5-none*)
+(typecheck-fail (t5-none**))
+
+;; This checks that X is not contravariant within (T5 X),
+;; by checking that X is not covariant within (→ (T5 X) Int).
+(define (t5->int [t5 : (T5 X)] → Int) 0)
+(define (t5->int* → (→ (T5 X) Int)) t5->int)
+(typecheck-fail (t5->int*))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Recursive Types
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T6 X) t6-none (t6-same (T6 X)))
+;; X should be inferred to be irrelevant within (T6 X).
+
+;; This checks that X is covariant within (T6 X).
+(define (t6-none* → (T6 X)) t6-none)
+(define (t6-none** → (→ (T6 X))) t6-none*)
+(check-type (t6-none**) : (→/test (T6 X)))
+
+;; This checks that X is contravariant within (T6 X),
+;; by checking that X is covariant within (→ (T6 X) Int).
+(define (t6->int [t6 : (T6 X)] → Int) 0)
+(define (t6->int* → (→ (T6 X) Int)) t6->int)
+(check-type (t6->int*) : (→/test (T6 X) Int))
+
+;; This checks that X is irrelevant, even within a Ref type,
+;; by checking that X is covariant within (Ref (T6 X)).
+;; This is still sound because a value of type (Ref (T6 X)) will never
+;; contain anything of type X anyway. X is irrelevant within it.
+(define (ref-t6* → (Ref (T6 X))) (ref (t6-none {X})))
+(define (ref-t6** → (→ (Ref (T6 X)))) ref-t6*)
+(check-type (ref-t6**) : (→/test (Ref (T6 X))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T7 X) t7-none (t7-weird (→ (T7 X) Int)))
+(define-type (T8 X) t8-none (t8-weird (T8 (→ X Int))))
+(define-type (T9 X) t9-none (t9-weird (→ (T9 (→ X Int)) Int)))
+;; X should be inferred to be irrelevant within (T7 X), (T8 X), and
+;; (T9 X). None of these types could contain or recieve an actual X.
+
+(define-type (T10 X) (t10 (T7 X) (T8 X) (T9 X)))
+;; So because of that, X should be irrelevant within (T10 X).
+
+;; This checks that X is covariant within (T10 X).
+(define (t10-none* → (T10 X)) (t10 t7-none t8-none t9-none))
+(define (t10-none** → (→ (T10 X))) t10-none*)
+(check-type (t10-none**) : (→/test (T10 X)))
+
+;; This checks that X is contravariant within (T10 X),
+;; by checking that X is covariant within (→ (T10 X) Int).
+(define (t10->int [t10 : (T10 X)] → Int) 0)
+(define (t10->int* → (→ (T10 X) Int)) t10->int)
+(check-type (t10->int*) : (→/test (T10 X) Int))
+
+;; This checks that X is irrelevant, even within a Ref type,
+;; by checking that X is covariant within (Ref (T10 X)).
+;; This is still sound because a value of type (Ref (T10 X)) will never
+;; contain anything of type X anyway. X is irrelevant within it.
+(define (ref-t10* → (Ref (T10 X))) (ref (t10 (t7-none {X}) (t8-none {X}) (t9-none {X}))))
+(define (ref-t10** → (→ (Ref (T10 X)))) ref-t10*)
+(check-type (ref-t10**) : (→/test (Ref (T10 X))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T11 X) t11-none (t11+ X) (t11-weird (→ (T11 X) Int)))
+(define-type (T12 X) t12-none (t12+ X) (t12-weird (T12 (→ X Int))))
+(define-type (T13 X) t13-none (t13+ X)
+  (t13-weird (→ (T13 (→ X Int)) Int)))
+(define-type (T14 X) t14-none (t14- (→ X Int))
+  (t14-weird (→ (T14 (→ X Int)) Int)))
+;; X should be inferred to be invariant within (T11 X) and (T12 X),
+;; but covariant within (T13 X), and contravariant within (T14 X).
+
+;; This checks that X is covariant within (T13 X), but not any of the
+;; others.
+(define (t11-none* → (T11 X)) t11-none)
+(define (t12-none* → (T12 X)) t12-none)
+(define (t13-none* → (T13 X)) t13-none)
+(define (t14-none* → (T14 X)) t14-none)
+(define (t11-none** → (→ (T11 X))) t11-none*)
+(define (t12-none** → (→ (T12 X))) t12-none*)
+(define (t13-none** → (→ (T13 X))) t13-none*)
+(define (t14-none** → (→ (T14 X))) t14-none*)
+(typecheck-fail (t11-none**))
+(typecheck-fail (t12-none**))
+(check-type (t13-none**) : (→/test (T13 X)))
+(typecheck-fail (t14-none**))
+
+;; This checks that X is contravariant within (T14 X), but not any of
+;; the others.
+(define (t11->int [t11 : (T11 X)] → Int) 0)
+(define (t12->int [t12 : (T12 X)] → Int) 0)
+(define (t13->int [t13 : (T13 X)] → Int) 0)
+(define (t14->int [t14 : (T14 X)] → Int) 0)
+(define (t11->int* → (→ (T11 X) Int)) t11->int)
+(define (t12->int* → (→ (T12 X) Int)) t12->int)
+(define (t13->int* → (→ (T13 X) Int)) t13->int)
+(define (t14->int* → (→ (T14 X) Int)) t14->int)
+(typecheck-fail (t11->int*))
+(typecheck-fail (t12->int*))
+(typecheck-fail (t13->int*))
+(check-type (t14->int*) : (→/test (T14 X) Int))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T15 X) t15-none (t15-cons+ X (T15 X)))
+(define-type (T16 X) t16-none (t16-cons- (→ X Int) (T16 X)))
+;; X should be inferred to be covariant within (T15 X), and
+;; contravariant within (T16 X). (T15 X) is just like a (List X) type,
+;; and (T16 X) is just like a (List (→ X Int)).
+
+;; This checks that X is covariant within (T15 X).
+(define (t15-none* → (T15 X)) t15-none)
+(define (t15-none** → (→ (T15 X))) t15-none*)
+(check-type (t15-none**) : (→/test (T15 X)))
+;; This checks that X is not covariant within (T16 X).
+(define (t16-none* → (T16 X)) t16-none)
+(define (t16-none** → (→ (T16 X))) t16-none*)
+(typecheck-fail (t16-none**))
+
+;; This checks that X is not contravariant within (T15 X),
+;; by checking that X is not covariant within (→ (T15 X) Int).
+(define (t15->int [t15 : (T15 X)] → Int) 0)
+(define (t15->int* → (→ (T15 X) Int)) t15->int)
+(typecheck-fail (t15->int*))
+;; This checks that X is contravariant within (T16 X),
+;; by checking that X is covariant within (→ (T16 X) Int).
+(define (t16->int [t16 : (T16 X)] → Int) 0)
+(define (t16->int* → (→ (T16 X) Int)) t16->int)
+(check-type (t16->int*) : (→/test (T16 X) Int))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Mutually Recursive Types
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type (T17 X) (t17-some X) (t18 (T18 X)))
+(define-type (T18 X) t18-none (t18-cons (T17 X) (T18 X)))
+;; X should be inferred to be covariant in both (T17 X) and (T18 X).
+;; This is similar to an arbitrary-arity tree type.
+
+;; This checks that X is covariant within (T17 X).
+(define (t17-none* → (T17 X)) (t18 t18-none))
+(define (t17-none** → (→ (T17 X))) t17-none*)
+(check-type (t17-none**) : (→/test (T17 X)))
+;; This checks that X is covariant within (T18 X).
+(define (t18-none* → (T18 X)) t18-none)
+(define (t18-none** → (→ (T18 X))) t18-none*)
+(check-type (t18-none**) : (→/test (T18 X)))
+
+;; This checks that X is not contravariant within (T17 X),
+;; by checking that X is not covariant within (→ (T17 X) Int).
+(define (t17->int [t17 : (T17 X)] → Int) 0)
+(define (t17->int* → (→ (T17 X) Int)) t17->int)
+(typecheck-fail (t17->int*))
+;; This checks that X is not contravariant within (T18 X),
+;; by checking that X is not covariant within (→ (T18 X) Int).
+(define (t18->int [t18 : (T18 X)] → Int) 0)
+(define (t18->int* → (→ (T18 X) Int)) t18->int)
+(typecheck-fail (t18->int*))
+

tapl/tests/run-mlish-tests1.rkt

@@ -6,6 +6,7 @@
 (require "mlish/polyrecur.mlish")
 (require "mlish/loop.mlish")
 (require "mlish/value-restriction-example.mlish")
+(require "mlish/infer-variances.mlish")
 
 ;; (require "mlish/trees.mlish")
 ;; (require "mlish/chameneos.mlish")

tapl/variance-constraints.rkt

@@ -0,0 +1,389 @@
+#lang racket/base
+
+(provide solve-variance-constraints
+         variance-mapping
+         variance=
+         variance-var
+         variance-join/expr
+         variance-compose/expr
+         variance-mapping-ref
+         )
+
+(require racket/bool
+         racket/list
+         racket/match
+         racket/set
+         (only-in (for-template "typecheck.rkt")
+                  variance?
+                  irrelevant
+                  covariant
+                  contravariant
+                  invariant
+                  variance-irrelevant?
+                  variance-covariant?
+                  variance-contravariant?
+                  variance-invariant?
+                  variance-join
+                  variance-compose
+                  ))
+
+(module+ test
+  (require rackunit))
+
+;; variance<=? : Variance Variance -> Boolean
+;; irrelevant < covariant
+;; irrelevant < contravariant
+;; covariant < invariant
+;; contravariant < invariant
+(define (variance<=? v1 v2)
+  (and (implies (variance-covariant? v2)
+                (variance-covariant? v1))
+       (implies (variance-contravariant? v2)
+                (variance-contravariant? v1))))
+
+;; A Variance-Constraint is a (variance= Variance-Expr Variance-Expr)
+(struct variance= (v1 v2) #:prefab)
+;; variance<= : Variance-Expr Variance-Expr -> Variance-Constraint
+(define (variance<= v1 v2)
+  (variance= (variance-expr-join v1 v2) v2))
+
+;; A Variance-Expr is one of:
+;;  - Variance-Var
+;;  - Variance
+;;  - (variance-expr-join Variance-Expr Variance-Expr)
+;;  - (variance-expr-compose Variance-Expr Variance-Expr)
+(struct variance-expr-join (v1 v2) #:prefab)
+(struct variance-expr-compose (v1 v2) #:prefab)
+
+;; A Variance-Var is a Symbol
+(define (variance-var sym) sym)
+(define (variance-var? v) (symbol? v))
+(define (variance-var=? v1 v2) (symbol=? v1 v2))
+
+;; A Variance-Mapping is a (Hashof Variance-Var Variance-Expr)
+;; variance-mapping : -> Variance-Mapping
+(define (variance-mapping) (hash))
+;; variance-mapping-has? : Variance-Mapping Variance-Var -> Boolean
+(define (variance-mapping-has? mapping var)
+  (hash-has-key? mapping var))
+;; variance-mapping-ref : Variance-Mapping Variance-Var -> Variance-Expr
+(define (variance-mapping-ref mapping var)
+  (hash-ref mapping var))
+;; variance-mapping-set : Variance-Mapping Variance-Var Variance-Expr -> Variance-Mapping
+(define (variance-mapping-set mapping var variance)
+  (hash-set mapping var variance))
+
+;; An Unfinished-Mapping is a (Hashof Variance-Var Variance)
+;; If a var is mapped to something in an Unfinished-Mapping, that
+;; means that the var is at least as restrictive as the variance it's
+;; mapped to.
+(define (unfinished-mapping-ref mapping var)
+  (hash-ref mapping var irrelevant))
+(define (unfinished-mapping-set mapping var value)
+  (hash-update mapping var (λ (v) (variance-join v value)) irrelevant))
+
+;; solve-variance-constraints :
+;; (Listof Variance-Var) (Listof Variance-Constraint) Variance-Mapping
+;; -> (U False Variance-Mapping)
+(define (solve-variance-constraints vars constraints mapping)
+  (match constraints
+    [(list)
+     (variance-mapping-interp-exprs vars mapping)]
+    [(cons constraint rest-cs)
+     (match constraint
+       [(variance= (? variance? v1) (? variance? v2))
+        (and
+         (equal? v1 v2)
+         (solve-variance-constraints vars rest-cs mapping))]
+       [constraint
+        (define free-vars (variance-constraint-variables #false constraint '()))
+        (cond
+          [(empty? free-vars)
+           (match-define (variance= v1 v2) constraint)
+           (solve-variance-constraints
+            vars
+            (cons (variance= (variance-expr-interp free-vars v1 mapping)
+                             (variance-expr-interp free-vars v2 mapping))
+                  rest-cs)
+            mapping)]
+          [else
+           (define valss
+             (for/list ([var (in-list free-vars)])
+               (list irrelevant covariant contravariant invariant)))
+           (for/or ([vals (in-list (apply cartesian-product valss))])
+             (define-values [constraints* mapping*]
+               (for/fold ([constraints constraints] [mapping mapping])
+                         ([var (in-list free-vars)]
+                          [val (in-list vals)])
+                 (values (variance-constraints-substitute constraints var val)
+                         (variance-mapping-set/substitute mapping var val))))
+             (solve-variance-constraints vars constraints* mapping*))])])]))
+
+;; variance-expr-substitute : Variance-Expr Variance-Var Variance-Expr -> Variance-Expr
+(define (variance-expr-substitute expr var value)
+  (match expr
+    [(? variance-var? v) (if (variance-var=? v var) value v)]
+    [(? variance? v) v]
+    [(variance-expr-join v1 v2)
+     (variance-expr-join (variance-expr-substitute v1 var value)
+                         (variance-expr-substitute v2 var value))]
+    [(variance-expr-compose v1 v2)
+     (variance-expr-compose (variance-expr-substitute v1 var value)
+                            (variance-expr-substitute v2 var value))]))
+
+;; variance-constraint-substitute :
+;; Variance-Constraint Variance-Var Variance-Expr -> Variance-Constraint
+(define (variance-constraint-substitute constraint var value)
+  (match constraint
+    [(variance= v1 v2)
+     (variance= (variance-expr-substitute v1 var value)
+                (variance-expr-substitute v2 var value))]))
+
+;; variance-constraints-substitute :
+;; (Listof Variance-Constraint) Variance-Var Variance-Expr -> (Listof Variance-Constraint)
+(define (variance-constraints-substitute constraints var value)
+  (for/list ([constraint (in-list constraints)])
+    (variance-constraint-substitute constraint var value)))
+
+;; variance-mapping-set/substitute : Variance-Mapping Variance-Var Variance-Expr -> Variance-Mapping
+(define (variance-mapping-set/substitute mapping var value)
+  (variance-mapping-set
+   (for/hash ([(k v) (in-hash mapping)])
+     (values k (variance-expr-substitute v var value)))
+   var value))
+
+;; variance-constraint-variables : (Listof Variance-Var) Variance-Constraint [(Setof Variance-Var)] -> (Setof Variance-Var)
+(define (variance-constraint-variables vars constraint [acc (seteq)])
+  (match constraint
+    [(variance= v1 v2)
+     (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))]))
+
+;; variance-expr-variables :
+;; (Listof Variance-Var) Variance-Expr [(Setof Variance-Var)] -> (Setof Variance-Var)
+(define (variance-expr-variables vars expr [acc (seteq)])
+  (match expr
+    [(? variance-var? v)
+     (if (implies vars (member v vars)) (set-add acc v) acc)]
+    [(? variance? v)
+     acc]
+    [(variance-expr-join v1 v2)
+     (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))]
+    [(variance-expr-compose v1 v2)
+     (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))]))
+
+;; variance-mapping-interp-exprs : (Listof Variance-Var) Variance-Mapping -> Variance-Mapping
+(define (variance-mapping-interp-exprs vars mapping)
+  (for/fold ([mapping mapping])
+            ([(k v) (in-hash mapping)])
+    (variance-mapping-set mapping k (variance-expr-interp vars v mapping))))
+
+;; variance-expr-interp : (Listof Variance-Var) Variance-Expr Variance-Mapping -> Variance-Expr
+(define (variance-expr-interp vars expr mapping)
+  (match expr
+    [(? variance? v) v]
+    [(? variance-var? v)
+     (cond
+       [(variance-mapping-has? mapping v)
+        (define expr (variance-mapping-ref mapping v))
+        (cond [(member v (variance-expr-variables #f expr '()))
+               (error 'variance-expr-interp "bad stufs is happening right now:\n~v = ~v" v expr)
+               v]
+              [else
+               (variance-expr-interp vars expr mapping)])]
+       [else v])]
+    [(variance-expr-join v1 v2)
+     (variance-join/expr (variance-expr-interp vars v1 mapping)
+                         (variance-expr-interp vars v2 mapping))]
+    [(variance-expr-compose v1 v2)
+     (variance-compose/expr (variance-expr-interp vars v1 mapping)
+                            (variance-expr-interp vars v2 mapping))]))
+
+;; variance-join/expr : Variance-Expr Variance-Expr -> Variance-Expr
+(define/match (variance-join/expr v1 v2)
+  [[(? variance? v1) (? variance? v2)] (variance-join v1 v2)]
+  [[(? variance? (? variance-invariant? v1)) _] v1]
+  [[_ (? variance? (? variance-invariant? v2))] v2]
+  [[(? variance? (? variance-irrelevant? v1)) v2] v2]
+  [[v1 (? variance? (? variance-irrelevant? v2))] v1]
+  [[v1 v2] #:when (equal? v1 v2) v1]
+  [[v1 v2] (variance-expr-join v1 v2)])
+
+;; variance-compose/expr : Variance-Expr Variance-Expr -> Variance-Expr
+(define/match (variance-compose/expr v1 v2)
+  [[(? variance? v1) (? variance? v2)] (variance-compose v1 v2)]
+  [[(? variance? (? variance-irrelevant? v1)) _] v1]
+  [[_ (? variance? (? variance-irrelevant? v2))] v2]
+  [[(? variance? (? variance-invariant? v1)) _] v1]
+  [[_ (? variance? (? variance-invariant? v2))] v2]
+  [[(? variance? (? variance-covariant? v1)) v2] v2]
+  [[v1 (? variance? (? variance-covariant? v2))] v1]
+  [[v1 v2] (variance-expr-compose v1 v2)])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(module+ test
+  (test-case "variance<=?"
+    (test-case "irrelevant <= everything"
+      (check-true (variance<=? irrelevant irrelevant))
+      (check-true (variance<=? irrelevant covariant))
+      (check-true (variance<=? irrelevant contravariant))
+      (check-true (variance<=? irrelevant invariant)))
+    (test-case "nothing else is <= irrelevant"
+      (check-false (variance<=? covariant irrelevant))
+      (check-false (variance<=? contravariant irrelevant))
+      (check-false (variance<=? invariant irrelevant)))
+    (test-case "everything <= invariant"
+      (check-true (variance<=? irrelevant invariant))
+      (check-true (variance<=? covariant invariant))
+      (check-true (variance<=? contravariant invariant))
+      (check-true (variance<=? invariant invariant)))
+    (test-case "invariant is not <= anything else"
+      (check-false (variance<=? invariant irrelevant))
+      (check-false (variance<=? invariant covariant))
+      (check-false (variance<=? invariant contravariant)))
+    (test-case "covariant and contravariant are not <= or >="
+      (check-false (variance<=? covariant contravariant))
+      (check-false (variance<=? contravariant covariant))))
+  (test-case "solve-variance-constraints"
+    (check-equal? (solve-variance-constraints
+                   (list) (list) (hash))
+                  (hash))
+    (check-equal? (solve-variance-constraints
+                   (list 'a) (list (variance= 'a irrelevant)) (hash))
+                  (hash 'a irrelevant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a) (list (variance= 'a covariant)) (hash))
+                  (hash 'a covariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a) (list (variance= 'a contravariant)) (hash))
+                  (hash 'a contravariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a) (list (variance= 'a invariant)) (hash))
+                  (hash 'a invariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a 'b)
+                   (list (variance= (variance-expr-compose covariant 'a)
+                                    (variance-expr-join covariant 'b)))
+                   (hash))
+                  (hash 'a covariant 'b irrelevant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-join
+                                      covariant
+                                      (variance-expr-compose
+                                       covariant
+                                       'a))
+                                     irrelevant)))
+                   (hash))
+                  (hash 'a covariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      contravariant
+                                      covariant)
+                                     irrelevant)))
+                   (hash))
+                  (hash 'a contravariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      contravariant
+                                      'a)
+                                     irrelevant)))
+                   (hash))
+                  (hash 'a irrelevant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      contravariant
+                                      'a)
+                                     covariant)))
+                   (hash))
+                  (hash 'a invariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      covariant
+                                      covariant)
+                                     (variance-expr-compose
+                                      contravariant
+                                      covariant))))
+                   (hash))
+                  (hash 'a invariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-join
+                                      (variance-expr-compose
+                                       covariant
+                                       'a)
+                                      (variance-expr-compose
+                                       contravariant
+                                       'a))
+                                     covariant)))
+                   (hash))
+                  (hash 'a invariant))
+    (check-equal? (solve-variance-constraints
+                   (list 'a 'b 'c 'd)
+                   (list (variance= 'a
+                                    (variance-expr-join
+                                     (variance-expr-join
+                                      (variance-expr-join
+                                       (variance-expr-compose
+                                        contravariant
+                                        covariant)
+                                       irrelevant)
+                                      (variance-expr-compose
+                                       covariant
+                                       'c))
+                                     (variance-expr-compose
+                                      irrelevant
+                                      'd)))
+                         (variance= 'b
+                                    (variance-expr-join
+                                     (variance-expr-join
+                                      (variance-expr-join
+                                       (variance-expr-compose
+                                        contravariant
+                                        irrelevant)
+                                       covariant)
+                                      (variance-expr-compose
+                                       covariant
+                                       'c))
+                                     (variance-expr-compose
+                                      covariant
+                                      'd)))
+                         (variance= 'c
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      covariant
+                                      'a)
+                                     (variance-expr-compose
+                                      covariant
+                                      'b)))
+                         (variance= 'd
+                                    (variance-expr-join
+                                     (variance-expr-compose
+                                      irrelevant
+                                      'a)
+                                     (variance-expr-compose
+                                      irrelevant
+                                      'd))))
+                   (hash))
+                  (hash 'a invariant
+                        'b invariant
+                        'c invariant
+                        'd irrelevant))
+    )
+  )