Use contract-neg-party to accurately handle contracted applications

Fixes #38
This commit is contained in:
Alexis King 2015-03-03 16:15:09 -08:00
parent 766bd83a98
commit 3f67cfea7c
2 changed files with 25 additions and 1 deletions

View File

@ -18,7 +18,7 @@
(define-tc/app-syntax-class (tc/app-contracts expected)
(pattern (ctc-id:id blame e ...)
;; check that this is an application from the contract system
#:when (contract-rename-id-property #'ctc-id)
#:when (contract-neg-party-property #'ctc-id)
(check-contract #'ctc-id #'(e ...) expected)))
;; Assume that the contracted thing is of the same type the type

View File

@ -0,0 +1,24 @@
#lang racket
(module untyped racket
(provide
(contract-out
[f (-> number? number? number?)]
[g (case-> (-> number? number? number?))]))
(define (f x y)
(expt x y))
(define (g x y)
(expt x y)))
(module type-env typed-racket/base-env/extra-env-lang
(require (submod ".." untyped))
(type-environment
[f (-> -Number -Number -Number)]
[g (-> -Number -Number -Number)]))
(module typed typed/racket
(require (submod ".." type-env)
typed/rackunit)
(check-equal? (f 2 4) (g 2 4)))
(require 'typed)