Generate trivial constraints for missing type variables.

If the type variable isn't mentioned anywhere, then just
pick `Any` as its substitution.

Fixes #152.
This commit is contained in:
Sam Tobin-Hochstadt 2015-06-23 13:10:17 -04:00
parent 6bef6e6ca8
commit 9a2b74dc33
4 changed files with 39 additions and 27 deletions

View File

@ -735,7 +735,7 @@
;; R : Type/c - result type into which we will be substituting
(define/cond-contract (subst-gen C X Y R)
(cset? (listof symbol?) (listof symbol?) (or/c Values/c AnyValues? ValuesDots?)
. -> . (or/c #f substitution/c))
. -> . (or/c #f substitution/c))
(define var-hash (free-vars-hash (free-vars* R)))
(define idx-hash (free-vars-hash (free-idxs* R)))
;; c : Constaint
@ -772,32 +772,35 @@
S))
(match (car (cset-maps C))
[(cons cmap (dmap dm))
(let ([subst (hash-union
(let* ([subst (hash-union
(for/hash ([(k dc) (in-hash dm)])
(define (c->t c) (constraint->type c (hash-ref idx-hash k Constant)))
(values
k
(match dc
[(dcon fixed #f)
(i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred
(map c->t fixed)
(c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted
(map c->t fixed)
(c->t dc)
dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k Constant))))))])
k
(match dc
[(dcon fixed #f)
(i-subst (map c->t fixed))]
[(or (dcon fixed rest) (dcon-exact fixed rest))
(i-subst/starred
(map c->t fixed)
(c->t rest))]
[(dcon-dotted fixed dc dbound)
(i-subst/dotted
(map c->t fixed)
(c->t dc)
dbound)])))
(for/hash ([(k v) (in-hash cmap)])
(values k (t-subst (constraint->type v (hash-ref var-hash k Constant))))))]
[subst (for/fold ([subst subst]) ([v (in-list X)])
(let ([entry (hash-ref subst v #f)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
;; If we don't have one, there are no constraints on this variable
(if (and entry (t-subst? entry))
subst
(hash-set subst v (t-subst Univ)))))])
;; verify that we got all the important variables
(and (for/and ([v (in-list X)])
(let ([entry (hash-ref subst v #f)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
(and entry (t-subst? entry))))
(extend-idxs subst)))]))
(extend-idxs subst))]))
;; context : the context of what to infer/not infer
;; S : a list of types to be the subtypes of T

View File

@ -5,7 +5,7 @@
"utils.rkt"
syntax/parse racket/match
syntax/parse/experimental/reflect
(typecheck signatures tc-funapp)
"../signatures.rkt" "../tc-funapp.rkt"
(types utils)
(rep type-rep filter-rep object-rep))

View File

@ -1,7 +1,7 @@
#lang racket/base
(require (rename-in "../utils/utils.rkt" [infer r:infer])
racket/match
racket/match racket/list
(prefix-in c: (contract-req))
(env tvar-env)
(for-syntax syntax/parse racket/base)
@ -98,8 +98,8 @@
;; in filters/objects).
(λ (dom rng rest kw? a)
(extend-tvars vars
(infer/vararg vars null argtys dom rest rng
(and expected (tc-results->values expected)))))
(infer/vararg vars null argtys dom rest rng
(and expected (tc-results->values expected)))))
f-type args-res expected)]
;; Row polymorphism. For now we do really dumb inference that only works
;; in very restricted cases, but is probably enough for most cases in

View File

@ -0,0 +1,9 @@
#lang typed/racket/base
(: f : (All (A) (case-> [-> Zero]
[A -> A])))
(define f
(case-lambda
[() 0]
[(a) a]))
(define (f0)
(f))