diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index bcfc0e85fb..dfc1c980c4 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -255,6 +255,9 @@ [(a a) empty] [(_ (Univ:)) empty] + [((Refinement: S _ _) T) + (cg S T)] + [((F: (? (lambda (e) (memq e X)) v)) S) (when (match S [(F: v*) diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 68de466788..ccfc78c818 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -220,6 +220,9 @@ (unmatch)) ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] + ;; A refinement is a subtype of its parent + [(list (Refinement: par _ _) t) + (subtype* A0 par t)] ;; use unification to see if we can use the polytype here [(list (Poly: vs b) s) (=> unmatch) @@ -292,10 +295,7 @@ [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] ;; single values shouldn't actually happen, but they're just like the type [(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))] - [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))] - ;; A refinement is a subtype of its parent - [(list (Refinement: par _ _) t) - (subtype* A0 par t)] + [(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))] ;; subtyping on other stuff [(list (Syntax: t) (Syntax: t*)) (subtype* A0 t t*)] diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index b5852df8d3..5ee756b025 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -123,6 +123,8 @@ [(F: nm) (fp "~a" nm)] [(Values: (list v ...)) (fp "~a" (cons 'values v))] [(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))] + [(Refinement: parent p? _) + (fp "(Refinement ~a ~a)" parent (syntax-e p?))] [(Param: in out) (if (equal? in out) (fp "(Parameter ~a)" in)