Improve check-below errors for classes/objects

Also fix a type-checker bug that the tests for the
error messages uncovered.
This commit is contained in:
Asumu Takikawa 2015-01-20 10:49:28 -05:00
parent b9aca78cf0
commit 4ab7ba2578
5 changed files with 275 additions and 78 deletions

View File

@ -6,7 +6,7 @@
(types utils union subtype filter-ops abbrev)
(utils tc-utils)
(rep type-rep object-rep filter-rep)
(only-in (types printer) pretty-format-type))
(typecheck error-message))
(provide/cond-contract
[check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
@ -15,10 +15,9 @@
[cond-check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
[t (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))])
[_ (s) (-or/c #f (if (Type/c? s) Type/c full-tc-results/c))])]
[fix-results (--> tc-results/c full-tc-results/c)]
[type-mismatch (-->* ((-or/c Type/c string?) (-or/c Type/c string?))
((-or/c string? #f))
-any)])
[fix-results (--> tc-results/c full-tc-results/c)])
(provide type-mismatch)
(define (print-object o)
(match o
@ -30,14 +29,6 @@
(define (cond-check-below tr1 expected)
(if expected (check-below tr1 expected) tr1))
;; type-mismatch : Any Any [String] -> Void
;; Type errors with "type mismatch", arguments may be types or other things
;; like the length of a list of types
(define (type-mismatch t1 t2 [more #f])
(define t1* (if (Type/c? t1) (pretty-format-type t1 #:indent 12) t1))
(define t2* (if (Type/c? t2) (pretty-format-type t2 #:indent 9) t2))
(tc-error/fields "type mismatch" #:more more "expected" t1* "given" t2* #:delayed? #t))
;; value-mismatch : tc-results/c tc-results/c -> void?
;; Helper to print messages of the form
;; "Expecte n values, but got m values"
@ -54,25 +45,6 @@
(value-string expected) (value-string actual)
"mismatch in number of values"))
;; expected-but-got : (U Type String) (U Type String) -> Void
;;
;; Helper to print messages of the form
;; "Expected a, but got b"
;;
;; Also handles cases like two type variables that
;; have the same name.
(define (expected-but-got t1 t2)
(match* (t1 t2)
[((F: s1) (F: s2))
(=> fail)
(unless (string=? (symbol->string s1) (symbol->string s2))
(fail))
;; FIXME: this case could have a better error message that, say,
;; prints the binding locations of each type variable.
(type-mismatch (format "`~a'" t1) (format "a different `~a'" t2)
"type variables bound in different scopes")]
[(_ _) (type-mismatch t1 t2)]))
;; fix-filter: FilterSet [FilterSet] -> FilterSet
;; Turns NoFilter into the actual filter; leaves other filters alone.
(define (fix-filter f [f2 -top-filter])

View File

@ -489,8 +489,6 @@
super-field-names
super-method-names
super-augment-names)
(when expected
(check-below final-class-type expected))
(define class-type-parameters (hash-ref parse-info 'type-parameters))
(do-timestamp "done")
(if (null? class-type-parameters)
@ -568,35 +566,6 @@
optional-external
remaining-super-inits
super-field-names super-method-names super-augment-names)
(when expected
(match-define (Class: _ inits fields methods augments _) expected)
(define exp-init-names (dict-keys inits))
(define exp-field-names (dict-keys fields))
(define exp-method-names (dict-keys methods))
(define exp-augment-names (dict-keys augments))
(define exp-optional-inits
(for/set ([(name val) (in-dict inits)]
#:when (cadr val))
name))
(check-same (set-union (hash-ref parse-info 'init-names)
(dict-keys remaining-super-inits))
exp-init-names
"initialization argument")
(check-same (set-union (hash-ref parse-info 'public-names)
(hash-ref parse-info 'pubment-names)
super-method-names)
exp-method-names
"public method")
(check-same (set-union (hash-ref parse-info 'field-names)
super-field-names)
exp-field-names
"public field")
(check-same (set-union (hash-ref parse-info 'augmentable-names)
super-augment-names)
exp-augment-names
"public augmentable method")
(check-same optional-external exp-optional-inits
"optional init argument"))
(check-exists super-method-names (hash-ref parse-info 'override-names)
"overridable method")
(check-exists super-augment-names (hash-ref parse-info 'augment-names)

View File

@ -0,0 +1,172 @@
#lang racket/base
;; This module provides helpers for producing type error messages
;; for check-below.
(require "../utils/utils.rkt"
(prefix-in - (contract-req))
racket/dict
racket/match
racket/set
(types utils subtype resolve)
(utils tc-utils)
(rep type-rep)
(only-in (types printer) pretty-format-type))
(provide/cond-contract [expected-but-got
(--> (-or/c Type/c string?)
(-or/c Type/c string?)
-any)]
[type-mismatch
(-->* ((-or/c Type/c string?) (-or/c Type/c string?))
((-or/c string? #f))
-any)])
;; type-mismatch : Any Any [String] -> Void
;; Type errors with "type mismatch", arguments may be types or other things
;; like the length of a list of types
(define (type-mismatch t1 t2 [more #f])
(define t1* (if (Type/c? t1) (pretty-format-type t1 #:indent 12) t1))
(define t2* (if (Type/c? t2) (pretty-format-type t2 #:indent 9) t2))
(tc-error/fields "type mismatch" #:more more "expected" t1* "given" t2* #:delayed? #t))
;; expected-but-got : (U Type String) (U Type String) -> Void
;;
;; Helper to print messages of the form
;; "Expected a, but got b"
;;
;; Also handles special cases like when two type variables
;; have the same name but are different. Or for types that are too
;; long for a subtyping error to be helpful directly.
(define (expected-but-got t1 t2)
(define r1 (resolve t1))
(define r2 (resolve t2))
(match* (r1 r2)
[((F: s1) (F: s2))
(=> fail)
(unless (string=? (symbol->string s1) (symbol->string s2))
(fail))
;; FIXME: this case could have a better error message that, say,
;; prints the binding locations of each type variable.
(type-mismatch (format "`~a'" t1) (format "a different `~a'" t2)
"type variables bound in different scopes")]
[((? Class?) (? Class?))
(class-mismatch r1 r2)]
[((Instance: c1) (Instance: c2))
(define r1 (resolve c1))
(define r2 (resolve c2))
(class-mismatch r1 r2 #t)]
;; Don't call this with resolved types since we may want to print
;; the type alias name instead of the actual type
[(_ _) (type-mismatch t1 t2)]))
;; class-mismatch : Class Class Boolean -> Void
;; Explains an expected/given type mismatch for cases with Class or Instance
;; types. In both cases, the Class type is passed in to generate the error
;; message (the object? argument distinguishes the cases).
(define (class-mismatch c1 c2 [object? #f])
(define class/object (if object? "object" "class"))
(match-define (Class: row inits fields methods augments init-rest) c1)
(match-define (Class: row* inits* fields* methods* augments* init-rest*) c2)
(when (not object?)
(when (and (F? row) (not (F? row*)))
(type-mismatch (format "Class with row variable `~a'" row)
(format "Class with no row variable")))
(when (and (F? row*) (not (F? row)))
(type-mismatch (format "Class with no row variable")
(format "Class with row variable `~a'" row*)))
(when (and (F? row) (F? row) (not (equal? row row*)))
(type-mismatch (format "Class with row variable `~a'" row)
(format "Class with row variable `~a'" row*))))
(define (missing-key kind map1 map2)
(define keys1 (map car map1))
(define keys2 (map car map2))
(cond [(not (set-empty? (set-subtract keys1 keys2)))
(define key (set-first (set-subtract keys1 keys2)))
(tc-error/expr/fields "type mismatch"
#:more
(format "~a lacks expected ~a `~a'" class/object kind key)
#:return #f)]
[(and (not object?)
(not (set-empty? (set-subtract keys2 keys1))))
(define key (set-first (set-subtract keys2 keys1)))
(tc-error/expr/fields "type mismatch"
#:more
(format "class has ~a `~a' that is not in expected type" kind key)
#:return #f)]
[;; init arguments out of order
(and (equal? kind "init")
(not object?)
(set=? keys1 keys2)
(not (equal? keys1 keys2)))
(tc-error/expr/fields "type mismatch"
#:more
"mismatch in initialization argument order"
"expected" keys1
"given" keys2
#:return #f)]
[else #t]))
(define (subtype-clauses kind map1 map2)
(define keys1 (map car map1))
(define keys2 (map car map2))
(define both-keys (set-intersect keys1 keys2))
(for/and ([key (in-list both-keys)])
(define entry1 (dict-ref map1 key))
(define entry2 (dict-ref map2 key))
(cond [;; a field or method
(null? (cdr entry1))
(or (subtype (car entry2) (car entry1))
(tc-error/expr/fields "type mismatch"
#:more (format "wrong type for ~a `~a'" kind key)
"expected" (car entry1)
"given" (car entry2)
#:return #f))]
[;; an init arg
else
(match-define (list type1 optional?1) entry1)
(match-define (list type2 optional?2) entry2)
(and (or (subtype type2 type1)
(tc-error/expr/fields "type mismatch"
#:more (format "wrong type for ~a `~a'" kind key)
"expected" (car entry1)
"given" (car entry2)
#:return #f))
(or (equal? optional?1 optional?2)
(tc-error/expr/fields "type mismatch"
"expected"
(format "~a init `~a'"
(if optional?1 "optional" "mandatory")
key)
"given"
(format "~a init `~a'"
(if optional?2 "optional" "mandatory")
key)
#:return #f)))])))
(define (check-init-rest ir1 ir2)
(and (or (not (and ir1 (not ir2)))
(tc-error/expr/fields "type mismatch"
"expected" "Class with init-rest type"
"given" "Class with no init-rest type"
#:return #f))
(or (not (and ir2 (not ir1)))
(tc-error/expr/fields "type mismatch"
"expected" "Class with no init-rest type"
"given" "Class with init-rest type"
#:return #f))
(or (not (and ir1 ir2))
(subtype ir2 ir1)
(tc-error/expr/fields "type mismatch"
#:more "wrong type for init-rest clause"
"expected" ir1
"given" ir2
#:return #f))))
(and (or object?
(and (missing-key "init" inits inits*)
(missing-key "augmentable method" augments augments*)
(subtype-clauses "init" inits inits*)
(subtype-clauses "augmentable method" augments augments*)
(check-init-rest init-rest init-rest*)))
(missing-key "method" methods methods*)
(missing-key "field" fields fields*)
(subtype-clauses "method" methods methods*)
(subtype-clauses "field" fields fields*)))

View File

@ -656,7 +656,9 @@
(equal-clause? fields fields*)
(equal-clause? methods methods*)
(equal-clause? augments augments*)
(sub init-rest init-rest*))]
(or (and init-rest init-rest*
(sub init-rest init-rest*))
(and (not init-rest) (not init-rest*))))]
;; otherwise, not a subtype
[(_ _) #f])))
(when (null? A)

View File

@ -236,7 +236,7 @@
(define/public (m) 0)))
(void))
#:ret (ret -Void)
#:msg #rx"public method that should be absent.*method: m"]
#:msg #rx"method `m' that is not in expected type"]
;; same as previous
[tc-err (let ()
(: c% (Class [m (Integer -> Integer)]))
@ -245,7 +245,7 @@
(define/public (n) 0)))
(void))
#:ret (ret -Void)
#:msg #rx"public method that should be absent.*method: n"]
#:msg #rx"method `n' that is not in expected type"]
;; fails, too many inits
[tc-err (let ()
(: c% (Class))
@ -253,7 +253,7 @@
(init x)))
(void))
#:ret (ret -Void)
#:msg #rx"initialization argument that should be absent.*argument: x"]
#:msg #rx"init `x' that is not in expected type"]
;; fails, init should be optional but is mandatory
[tc-err (let ()
(: c% (Class (init [str String #:optional])))
@ -261,7 +261,7 @@
(init str)))
(void))
#:ret (ret -Void)
#:msg #rx"missing a required optional init argument.*argument: str"]
#:msg #rx"expected: optional init `str'.*given: mandatory init `str'"]
;; fails, too many fields
[tc-err (let ()
(: c% (Class (field [str String])))
@ -269,7 +269,7 @@
(field [str "foo"] [x 0])))
(void))
#:ret (ret -Void)
#:msg #rx"has a public field that should be absent.*public field: x"]
#:msg #rx"field `x' that is not in expected type"]
;; test that an init with no annotation still type-checks
;; (though it will have the Any type)
[tc-e (let () (class object% (super-new) (init x)) (void)) -Void]
@ -314,7 +314,7 @@
(mixin arg-class%))
#:ret (ret (-class #:method ([m (t:-> -Integer)] [n (t:-> -String)])))
#:msg #rx"missing a required public method.*missing public method: n"]
#:msg #rx"lacks expected method `n'"]
;; Fail, bad mixin argument
[tc-err (let ()
(: mixin ((Class [m (-> Symbol)])
@ -335,7 +335,7 @@
(mixin arg-class%)
(void))
#:ret (ret -Void)
#:msg #rx"expected: \\(Class \\(m \\(-> Symbol\\)\\)\\)"]
#:msg #rx"lacks expected method `m'"]
;; classes that don't use define/public directly
[tc-e (let ()
(: c% (Class [m (Number -> String)]))
@ -592,7 +592,7 @@
(init [x 0])))
(void))
#:ret (ret -Void)
#:msg #rx"has a optional init argument that should be absent"]
#:msg #rx"expected: mandatory init `x'.*given: optional init `x'"]
;; fails, mandatory init not provided
[tc-err (let ()
(define d% (class object% (super-new)
@ -766,7 +766,22 @@
(define x (new (class object% (super-new) (define/public (m) "m"))))
(ann x (Object [n (-> String)]))
(error "foo"))
#:msg #rx"expected: .*n.*given:.*m.*"]
#:msg #rx"lacks expected method `n'"]
[tc-err (let ()
(define x (new (class object% (super-new))))
(ann x (Object (field [x String])))
(error "foo"))
#:msg #rx"lacks expected field `x'"]
[tc-err (let ()
(define x (new (class object% (super-new) (define/public (m) "m"))))
(ann x (Object [m (-> Symbol)]))
(error "foo"))
#:msg #rx"expected: \\(-> Symbol\\).*given: \\(-> String"]
[tc-err (let ()
(define x (new (class object% (super-new) (field [x : Symbol 'x]))))
(ann x (Object (field [x String])))
(error "foo"))
#:msg #rx"expected: String.*given: Symbol"]
;; test use of `this` in field default
[tc-e (let ()
(class object%
@ -1017,7 +1032,7 @@
(mixin object%))
#:ret (ret (-class #:row (make-Row null null null null #f)
#:field ([x Univ])))
#:msg (regexp-quote "expected: (Class (field (x Any)))")]
#:msg #rx"lacks expected field `x'"]
;; mixin application succeeds
[tc-e (let ()
(: f (All (A #:row (field x))
@ -1373,7 +1388,7 @@
(field [x : Symbol 'a])))
(void))
#:ret (ret -Void)
#:msg #rx"expected: \\(Class \\(field \\(x String"]
#:msg #rx"expected: String.*given: Symbol"]
;; fails, but make sure it's not an internal error
[tc-err (class object% (super-new)
(define/pubment (foo x) 0)
@ -1602,7 +1617,7 @@
(super-new)
(define/public (bar) (void))))
(error "foo"))
#:msg "type mismatch.*required public method"]
#:msg "lacks expected method `foo'"]
[tc-e (let ()
(define-type-alias A% (Class (init [y Symbol])))
(define-type-alias B% (Class #:implements/inits A% (init [x String])))
@ -1642,7 +1657,7 @@
(super-new)
(init y x)))
(error "foo"))
#:msg "type mismatch"]
#:msg #rx"initialization argument order.*expected: \\(x y\\).*given: \\(y x\\)"]
;; PR 14669 (next two)
[tc-e (let ()
(define-type-alias A (Class [m (-> Any)]))
@ -1710,4 +1725,71 @@
(: bar (-> String String))
(define bar (lambda (x) x))
(bar "foo"))
(-class)]))
(-class)]
;; The next several tests are for check-below error messages for checking
;; expected types that are Class types
[tc-err (let ()
(: f (All (X #:row) (-> (Class #:row-var X) (Class #:row-var X))))
(define (f cls) (class object% (super-new)))
(error "foo"))
#:msg #rx"expected: Class with row variable `X.*given: Class with no row variable"]
[tc-err (let ()
(: f (All (X #:row) (-> (Class #:row-var X) (Class))))
(define (f cls) cls)
(error "foo"))
#:msg #rx"expected: Class with no row variable.*given: Class with row variable `X"]
[tc-err (let ()
(ann (class object% (super-new))
(Class (init [x String])))
(error "foo"))
#:msg #rx"lacks expected init `x'"]
[tc-err (let ()
(ann (class object% (super-new))
(Class (field [x String])))
(error "foo"))
#:msg #rx"lacks expected field `x'"]
[tc-err (let ()
(ann (class object% (super-new))
(Class [m (-> String)]))
(error "foo"))
#:msg #rx"lacks expected method `m'"]
[tc-err (let ()
(ann (class object% (super-new) (init [x : Symbol]))
(Class (init [x String])))
(error "foo"))
#:msg #rx"expected: String.*given: Symbol"]
[tc-err (let ()
(ann (class object% (super-new) (init [x : String "x"]))
(Class (init [x String])))
(error "foo"))
#:msg #rx"expected: mandatory init `x'.*given: optional init `x'"]
[tc-err (let ()
(ann (class object% (super-new) (init [x : String]))
(Class (init [x String #:optional])))
(error "foo"))
#:msg #rx"expected: optional init `x'.*given: mandatory init `x'"]
[tc-err (let ()
(ann (class object% (super-new) (field [x : Symbol 'x]))
(Class (field [x String])))
(error "foo"))
#:msg #rx"expected: String.*given: Symbol"]
[tc-err (let ()
(define c% (class object% (super-new) (define/public (m) (void))))
(ann c% (Class [m (-> String)]))
(error "foo"))
#:msg #rx"expected: \\(-> String\\).*given: \\(-> Void\\)"]
[tc-err (let ()
(ann (class object% (super-new) (init-rest [rst : (Listof String)]))
(Class))
(error "foo"))
#:msg #rx"expected: Class with no init-rest type.*given: Class with init-rest type"]
[tc-err (let ()
(ann (class object% (super-new))
(Class [init-rest (Listof Void)]))
(error "foo"))
#:msg #rx"expected: Class with init-rest type.*given: Class with no init-rest type"]
[tc-err (let ()
(ann (class object% (super-new) (init-rest [rst : (Listof String)]))
(Class (init-rest (Listof Void))))
(error "foo"))
#:msg #rx"expected: \\(Listof Void\\).*given: \\(Listof String\\)"]))