Allow expected type to have weaker filters and objects.

Closes PR 10729.
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-19 12:23:32 -05:00
parent 7e9313bad3
commit 9fe3747a19
4 changed files with 54 additions and 6 deletions

View File

@ -0,0 +1,15 @@
#lang typed/scheme
(: g ((U Integer #f) -> Integer))
(define (g x)
(cond
[(or (equal? x 0) (equal? x #f)) 0]
[else x]))
(define-type-alias Source (U Symbol #f))
(: source? (Any -> Boolean : Source))
(define (source? x)
(if (false? x)
#t
(symbol? x)))

View File

@ -0,0 +1,4 @@
#lang typed/scheme
(: lon? (Any -> Boolean : (Listof Number)))
(define (lon? x)
(and (list? x) (andmap number? x)))

View File

@ -0,0 +1,12 @@
#lang scheme/load
(module bar scheme
(define (f x) x)
(provide f))
(module foo typed/scheme
(require/typed 'bar (f (Node -> Integer)))
(define-struct: node ({x : Integer}))
(define-type-alias Node node))
(require 'foo)

View File

@ -5,7 +5,7 @@
(require syntax/kerncase mzlib/trace (require syntax/kerncase mzlib/trace
scheme/match (prefix-in - scheme/contract) scheme/match (prefix-in - scheme/contract)
"signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" "signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
(types utils convenience union subtype remove-intersect type-table) (types utils convenience union subtype remove-intersect type-table filter-ops)
(private-in parse-type type-annotation) (private-in parse-type type-annotation)
(rep type-rep) (rep type-rep)
(only-in (infer infer) restrict) (only-in (infer infer) restrict)
@ -170,6 +170,18 @@
;; (Type Results -> Type) ;; (Type Results -> Type)
;; (Type Type -> Type)) ;; (Type Type -> Type))
(define (check-below tr1 expected) (define (check-below tr1 expected)
(define (filter-better? f1 f2)
(match* (f1 f2)
[(f f) #t]
[((FilterSet: f1+ f1-) (FilterSet: f2+ f2-))
(and (implied-atomic? f2+ f1+)
(implied-atomic? f2- f1-))]
[(_ _) #f]))
(define (object-better? o1 o2)
(match* (o1 o2)
[(o o) #t]
[(o (or (NoObject:) (Empty:))) #t]
[(_ _) #f]))
(define (maybe-abstract r) (define (maybe-abstract r)
(define l (hash-ref to-be-abstr expected #f)) (define l (hash-ref to-be-abstr expected #f))
(define (sub-one proc i) (define (sub-one proc i)
@ -212,12 +224,17 @@
(cond (cond
[(not (subtype t1 t2)) [(not (subtype t1 t2))
(tc-error/expr "Expected ~a, but got ~a" t2 t1)] (tc-error/expr "Expected ~a, but got ~a" t2 t1)]
[(and (not (filter-equal? f1 f2)) [(and (not (filter-better? f1 f2))
(object-equal? o1 o2)) (object-better? o1 o2))
(tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)] (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)]
[(not (and (equal? f1 f2) (equal? o1 o2))) [(and (filter-better? f1 f2)
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]) (not (object-better? o1 o2)))
expected] (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)]
[(and (not (filter-better? f1 f2))
(not (object-better? o1 o2)))
(tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]
[else
expected])]
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound)) [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
(unless (andmap subtype t1 t2) (unless (andmap subtype t1 t2)
(tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1)))