Implement the occurs check
In the writeback phase, the typechecker now checks that it isn't replacing a type variable T with a type that contains T. It also does an occurs check in do_autoderef in order to avoid getting into an infinite chain of derefs. I'm a bit worried that there are more places where the occurs check needs to happen where I'm not doing it now, though. Closes #768
This commit is contained in:
parent
d7d4b4fc38
commit
2baaeab784
@ -184,6 +184,7 @@ export type_param;
|
||||
export unify;
|
||||
export variant_info;
|
||||
export walk_ty;
|
||||
export occurs_check_fails;
|
||||
|
||||
// Data types
|
||||
tag mode { mo_val; mo_alias(bool); }
|
||||
@ -655,6 +656,7 @@ fn walk_ty(cx: &ctxt, walker: ty_walk, ty: t) {
|
||||
ty_str. {/* no-op */ }
|
||||
ty_istr. {/* no-op */ }
|
||||
ty_type. {/* no-op */ }
|
||||
ty_task. {/* no-op */ }
|
||||
ty_native(_) {/* no-op */ }
|
||||
ty_box(tm) { walk_ty(cx, walker, tm.ty); }
|
||||
ty_vec(tm) { walk_ty(cx, walker, tm.ty); }
|
||||
@ -686,6 +688,9 @@ fn walk_ty(cx: &ctxt, walker: ty_walk, ty: t) {
|
||||
walk_ty(cx, walker, sub);
|
||||
for tp: t in tps { walk_ty(cx, walker, tp); }
|
||||
}
|
||||
ty_constr(sub, _) {
|
||||
walk_ty(cx, walker, sub);
|
||||
}
|
||||
ty_var(_) {/* no-op */ }
|
||||
ty_param(_,_) {/* no-op */ }
|
||||
}
|
||||
@ -1393,6 +1398,24 @@ fn type_param(cx: &ctxt, ty: &t) -> option::t[uint] {
|
||||
ret none;
|
||||
}
|
||||
|
||||
// Returns an ivec of all the type variables
|
||||
// occurring in t. It may contain duplicates.
|
||||
fn vars_in_type(cx:&ctxt, ty: &t) -> int[] {
|
||||
fn collect_var(cx:&ctxt, vars: &@mutable int[], ty: t) {
|
||||
alt struct(cx, ty) {
|
||||
ty_var(v) {
|
||||
*vars += ~[v];
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
}
|
||||
let rslt: @mutable int[] = @mutable (~[]);
|
||||
walk_ty(cx, bind collect_var(cx, rslt, _), ty);
|
||||
// Works because of a "convenient" bug that lets us
|
||||
// return a mutable ivec as if it's immutable
|
||||
ret *rslt;
|
||||
}
|
||||
|
||||
fn type_autoderef(cx: &ctxt, t: &ty::t) -> ty::t {
|
||||
let t1: ty::t = t;
|
||||
while true {
|
||||
@ -1990,6 +2013,28 @@ fn is_lval(expr: &@ast::expr) -> bool {
|
||||
}
|
||||
}
|
||||
|
||||
fn occurs_check_fails(tcx: &ctxt, sp: &option::t[span], vid: int, rt: &t)
|
||||
-> bool {
|
||||
// Occurs check!
|
||||
if ivec::member(vid, vars_in_type(tcx, rt)) {
|
||||
alt sp {
|
||||
some (s) {
|
||||
// Maybe this should be span_err -- however, there's an
|
||||
// assertion later on that the type doesn't contain
|
||||
// variables, so in this case we have to be sure to die.
|
||||
tcx.sess.span_fatal(s,
|
||||
"Type inference failed because I \
|
||||
could not find a type\n that's both of the form " +
|
||||
ty_to_str(tcx, ty::mk_var(tcx, (vid)))
|
||||
+ " and of the form " + ty_to_str(tcx, rt)
|
||||
+ ". Such a type would have to be infinitely \
|
||||
large.");
|
||||
}
|
||||
_ { ret true; }
|
||||
}
|
||||
}
|
||||
else { ret false; }
|
||||
}
|
||||
|
||||
// Type unification via Robinson's algorithm (Robinson 1965). Implemented as
|
||||
// described in Hoder and Voronkov:
|
||||
@ -2318,9 +2363,6 @@ mod unify {
|
||||
// TODO: rewrite this using tuple pattern matching when available, to
|
||||
// avoid all this rightward drift and spikiness.
|
||||
|
||||
// TODO: occurs check, to make sure we don't loop forever when
|
||||
// unifying e.g. 'a and option['a]
|
||||
|
||||
// Fast path.
|
||||
|
||||
if eq_ty(expected, actual) { ret ures_ok(expected); }
|
||||
@ -2694,9 +2736,15 @@ mod unify {
|
||||
}
|
||||
|
||||
// Fixups and substitutions
|
||||
fn fixup_vars(tcx: ty_ctxt, vb: @var_bindings, typ: t) -> fixup_result {
|
||||
fn subst_vars(tcx: ty_ctxt, vb: @var_bindings,
|
||||
// Takes an optional span - complain about occurs check violations
|
||||
// iff the span is present (so that if we already know we're going
|
||||
// to error anyway, we don't complain)
|
||||
fn fixup_vars(tcx: ty_ctxt, sp: &option::t[span],
|
||||
vb: @var_bindings, typ: t) -> fixup_result {
|
||||
fn subst_vars(tcx: ty_ctxt, sp: &option::t[span], vb: @var_bindings,
|
||||
unresolved: @mutable option::t[int], vid: int) -> t {
|
||||
// Should really return a fixup_result instead of a t, but fold_ty
|
||||
// doesn't allow returning anything but a t.
|
||||
if vid as uint >= ufindivec::set_count(vb.sets) {
|
||||
*unresolved = some(vid);
|
||||
ret ty::mk_var(tcx, vid);
|
||||
@ -2705,15 +2753,18 @@ mod unify {
|
||||
alt smallintmap::find[t](vb.types, root_id) {
|
||||
none. { *unresolved = some(vid); ret ty::mk_var(tcx, vid); }
|
||||
some(rt) {
|
||||
if occurs_check_fails(tcx, sp, vid, rt) {
|
||||
// Return the type unchanged, so we can error out downstream
|
||||
ret rt;
|
||||
}
|
||||
ret fold_ty(tcx,
|
||||
fm_var(bind subst_vars(tcx, vb, unresolved, _)),
|
||||
rt);
|
||||
fm_var(bind subst_vars(tcx, sp, vb, unresolved, _)), rt);
|
||||
}
|
||||
}
|
||||
}
|
||||
let unresolved = @mutable none[int];
|
||||
let rty =
|
||||
fold_ty(tcx, fm_var(bind subst_vars(tcx, vb, unresolved, _)),
|
||||
fold_ty(tcx, fm_var(bind subst_vars(tcx, sp, vb, unresolved, _)),
|
||||
typ);
|
||||
let ur = *unresolved;
|
||||
alt ur {
|
||||
@ -2721,13 +2772,14 @@ mod unify {
|
||||
some(var_id) { ret fix_err(var_id); }
|
||||
}
|
||||
}
|
||||
fn resolve_type_var(tcx: &ty_ctxt, vb: &@var_bindings, vid: int) ->
|
||||
fn resolve_type_var(tcx: &ty_ctxt, sp: &option::t[span],
|
||||
vb: &@var_bindings, vid: int) ->
|
||||
fixup_result {
|
||||
if vid as uint >= ufindivec::set_count(vb.sets) { ret fix_err(vid); }
|
||||
let root_id = ufindivec::find(vb.sets, vid as uint);
|
||||
alt smallintmap::find[t](vb.types, root_id) {
|
||||
none. { ret fix_err(vid); }
|
||||
some(rt) { ret fixup_vars(tcx, vb, rt); }
|
||||
some(rt) { ret fixup_vars(tcx, sp, vb, rt); }
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -879,7 +879,18 @@ fn do_autoderef(fcx: &@fn_ctxt, sp: &span, t: &ty::t) -> ty::t {
|
||||
let t1 = t;
|
||||
while true {
|
||||
alt structure_of(fcx, sp, t1) {
|
||||
ty::ty_box(inner) { t1 = inner.ty; }
|
||||
ty::ty_box(inner) {
|
||||
alt ty::struct(fcx.ccx.tcx, t1) {
|
||||
ty::ty_var(v1) {
|
||||
if ty::occurs_check_fails(fcx.ccx.tcx, some(sp), v1,
|
||||
ty::mk_box(fcx.ccx.tcx, inner)) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
_ {}
|
||||
}
|
||||
t1 = inner.ty;
|
||||
}
|
||||
ty::ty_res(_, inner, tps) {
|
||||
t1 = ty::substitute_type_params(fcx.ccx.tcx, tps, inner);
|
||||
}
|
||||
@ -942,7 +953,7 @@ fn do_fn_block_coerce(fcx: &@fn_ctxt, sp: &span, actual: &ty::t,
|
||||
|
||||
|
||||
fn resolve_type_vars_if_possible(fcx: &@fn_ctxt, typ: ty::t) -> ty::t {
|
||||
alt ty::unify::fixup_vars(fcx.ccx.tcx, fcx.var_bindings, typ) {
|
||||
alt ty::unify::fixup_vars(fcx.ccx.tcx, none, fcx.var_bindings, typ) {
|
||||
fix_ok(new_type) { ret new_type; }
|
||||
fix_err(_) { ret typ; }
|
||||
}
|
||||
@ -1073,7 +1084,8 @@ mod writeback {
|
||||
fn resolve_type_vars_in_type(fcx: &@fn_ctxt, sp: &span, typ: ty::t) ->
|
||||
option::t[ty::t] {
|
||||
if !ty::type_contains_vars(fcx.ccx.tcx, typ) { ret some(typ); }
|
||||
alt ty::unify::fixup_vars(fcx.ccx.tcx, fcx.var_bindings, typ) {
|
||||
alt ty::unify::fixup_vars(fcx.ccx.tcx, some(sp),
|
||||
fcx.var_bindings, typ) {
|
||||
fix_ok(new_type) { ret some(new_type); }
|
||||
fix_err(vid) {
|
||||
fcx.ccx.tcx.sess.span_err(sp,
|
||||
@ -1139,7 +1151,7 @@ mod writeback {
|
||||
if !wbcx.success { ret; }
|
||||
let var_id = lookup_local(wbcx.fcx, l.span, l.node.id);
|
||||
let fix_rslt =
|
||||
ty::unify::resolve_type_var(wbcx.fcx.ccx.tcx,
|
||||
ty::unify::resolve_type_var(wbcx.fcx.ccx.tcx, some(l.span),
|
||||
wbcx.fcx.var_bindings, var_id);
|
||||
alt fix_rslt {
|
||||
fix_ok(lty) { write::ty_only(wbcx.fcx.ccx.tcx, l.node.id, lty); }
|
||||
|
5
src/test/compile-fail/occurs-check-2.rs
Normal file
5
src/test/compile-fail/occurs-check-2.rs
Normal file
@ -0,0 +1,5 @@
|
||||
// error-pattern: Type inference failed because I could not find
|
||||
fn main() {
|
||||
let f = @f;
|
||||
f();
|
||||
}
|
4
src/test/compile-fail/occurs-check.rs
Normal file
4
src/test/compile-fail/occurs-check.rs
Normal file
@ -0,0 +1,4 @@
|
||||
// error-pattern: Type inference failed because I could not find
|
||||
fn main() {
|
||||
let f = @f;
|
||||
}
|
Loading…
Reference in New Issue
Block a user