Further improvements for TR's error messages.

Only the most permissive domains whose associated return type is
consistent with the expected type are shown in error messages.

For example, for a function with the following type:
Fixnum -> Fixnum
Integer -> Integer
and an expected type of Integer, only the latter domain is shown in
the error message.

original commit: e011ea00bd73fd8ac3b9c4afe4e1435dcaa27cdb
This commit is contained in:
Vincent St-Amour 2010-09-24 17:43:12 -04:00
commit 1fb2c973f0
4 changed files with 146 additions and 17 deletions

View File

@ -1,7 +1,8 @@
#lang scheme/base
(require "../utils/utils.rkt" racket/match unstable/list
(utils tc-utils) (rep type-rep) (types utils union abbrev))
(only-in srfi/1 unzip4) (only-in racket/list make-list)
(utils tc-utils) (rep type-rep) (types utils union abbrev subtype))
(provide (all-defined-out))
@ -59,20 +60,145 @@
""))]
[else
(let ([label (if expected "Types: " "Domains: ")]
[nl+spc (if expected "\n " "\n ")]
[pdoms (map make-printable doms)])
(string-append
label
(stringify (if expected
(map stringify-domain pdoms rests drests rngs)
(map stringify-domain pdoms rests drests))
nl+spc)
"\nArguments: "
arguments-str
"\n"
(if expected
(format "Expected result: ~a\n" (make-printable expected))
"")))]))
[nl+spc (if expected "\n " "\n ")])
;; we restrict the domains shown in the error messages to those that
;; are useful
(let-values ([(pdoms rngs rests drests) (possible-domains doms rests drests rngs expected)])
(let ([pdoms (map make-printable pdoms)])
(string-append
label
(stringify (if expected
(map stringify-domain pdoms rests drests rngs)
(map stringify-domain pdoms rests drests))
nl+spc)
"\nArguments: "
arguments-str
"\n"
(if expected
(format "Expected result: ~a\n" (make-printable expected))
"")))))]))
;; to avoid long and confusing error messages, in the case of functions with
;; multiple similar domains (<, >, +, -, etc.), we show only the domains that
;; are relevant to this specific error
;; this is done in several ways:
;; - if a case-lambda case is subsumed by another, we don't need to show it
;; (subsumed cases may be useful for their filter information, but this is
;; unrelated to error reporting)
;; - if we have an expected type, we don't need to show the domains for which
;; the result type is not a subtype of the expected type
;; - we can disregard domains that are more restricted than required to get
;; the expected type (or all but the most liberal domain when no type is
;; expected)
;; ex: if we have the 2 following possible domains for an operator:
;; Fixnum -> Fixnum
;; Integer -> Integer
;; and an expected type of Integer for the result of the application,
;; we can disregard the Fixnum domain since it imposes a restriction that
;; is not necessary to get the expected type
(define (possible-domains doms rests drests rngs expected)
;; is fun-ty subsumed by a function type in others?
(define (is-subsumed-in? fun-ty others)
;; assumption: domains go from more specific to less specific
;; thus, a domain can only be subsumed by another that is further down
;; the list.
;; this is reasonable because a more specific domain coming after a more
;; general domain would never be matched
;; a case subsumes another if the first one is a subtype of the other
(ormap (lambda (x) (subtype x fun-ty))
others))
(define expected-ty (and expected (match expected [(tc-result1: t) t])))
(define (returns-subtype-of-expected? fun-ty)
(or (not expected)
(match fun-ty
[(Function: (list (arr: _ rng _ _ _)))
(let ([rng (match rng
[(Values: (list (Result: t _ _)))
t]
[(ValuesDots: (list (Result: t _ _)) _ _)
t])])
(subtype rng expected-ty))])))
;; original info that the error message would have used
;; kept in case we discard all the cases
(define orig (map list doms rngs rests drests))
;; iterate in lock step over the function types we analyze and the parts
;; that we will need to print the error message, to make sure we throw
;; away cases consistently
(let loop ([cases (map (compose make-Function list make-arr)
doms
(map (match-lambda ; strip filters
[(Values: (list (Result: t _ _) ...))
(-values t)]
[(ValuesDots: (list (Result: t _ _) ...) _ _)
(-values t)])
rngs)
rests drests (make-list (length doms) null))]
;; the parts we'll need to print the error message
[parts orig]
;; accumulators
[candidates '()] ; from cases
[parts-acc '()]) ; from parts
;; discard subsumed cases (supertype modulo filters)
(if (not (null? cases))
(let ([head (car cases)] [tail (cdr cases)])
(if (is-subsumed-in? head tail)
(loop tail (cdr parts)
candidates parts-acc) ; we discard this one
(loop tail (cdr parts)
(cons head candidates) ; we keep this one
(cons (car parts) parts-acc))))
;; keep only the domains for which the associated function type
;; is consistent with the expected type
(let loop ([cases candidates]
[parts parts-acc]
;; accumulators
[candidates '()]
[parts-acc '()])
(if (not (null? cases))
(if (returns-subtype-of-expected? (car cases))
(loop (cdr cases) (cdr parts)
(cons (car cases) candidates) ; we keep this one
(cons (car parts) parts-acc))
(loop (cdr cases) (cdr parts)
candidates parts-acc)) ; we discard this one
;; among the domains that fit with the expected type, we only
;; need to keep the most liberal
;; since we only care about permissiveness of domains, we
;; reconstruct function types with a return type of any then test
;; for subtyping
(let ([fun-tys-ret-any
(map (match-lambda
[(Function: (list (arr: dom _ rest drest _)))
(make-Function (list (make-arr dom Univ rest drest null)))])
candidates)])
(let loop ([cases fun-tys-ret-any]
[parts parts-acc]
;; accumulators
;; final pass, we only need the parts to print the
;; error message
[parts-acc '()])
(if (not (null? cases))
;; if a case is a supertype of another, we discard it
(let ([head (car cases)])
(if (is-subsumed-in? head (remove head fun-tys-ret-any))
(loop (cdr cases) (cdr parts)
parts-acc) ; we discard this one
(loop (cdr cases) (cdr parts)
(cons (car parts) parts-acc)))) ; we keep this one
;; if we somehow eliminate all the cases (bogus expected
;; type) fall back to the showing extra cases
(unzip4 (if (null? parts-acc)
orig
(reverse parts-acc)))))))))))
(define (poly-fail t argtypes #:name [name #f] #:expected [expected #f])
(match t

View File

@ -140,7 +140,9 @@
(tc-error/expr
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches arities doms rests drests rngs (map tc-expr (syntax->list pos-args)) #f #f)))
(domain-mismatches arities doms rests drests rngs
(map tc-expr (syntax->list pos-args))
#f #f #:expected expected)))
(tc/funapp (car (syntax-e form)) kw-args
(ret (make-Function new-arities))
(map tc-expr (syntax->list pos-args)) expected)))]))

View File

@ -58,7 +58,7 @@
(tc-error/expr
#:return (or expected (ret (Un)))
(string-append "No function domains matched in function application:\n"
(domain-mismatches t doms rests drests rngs argtys-t #f #f))))]
(domain-mismatches t doms rests drests rngs argtys-t #f #f #:expected expected))))]
;; any kind of dotted polymorphic function without mandatory keyword args
[((tc-result1: (and t (PolyDots:
(and vars (list fixed-vars ... dotted-var))

View File

@ -83,6 +83,7 @@ don't depend on any other portion of the system
(define (reset!) (set! delayed-errors null))
(match (reverse delayed-errors)
[(list) (void)]
;; if there's only one, we don't need multiple-error handling
[(list (struct err (msg stx)))
(reset!)
(raise-typecheck-error msg stx)]