Implement the occurs check for type unification

We can infinite loop if we try to unify e.g. T with option[T]. Fixing this requires implementing the occurs check. Off the top of my head, I can't think of any cases in which we'd actually trip this, but it's theoretically possible.

Tim thinks this may also be the cause of segfaulting on infinitely interior tags:

tag t1 {
    a(int);
    b(@t1);
}

I think maybe some permutation of the following might trigger it:

fn f[T](T x) -> option[T] {
  auto y = f(Some(x));
  ret Some(t);
}

I'm not sure if this is exactly right but the idea is to try to write a function that forces the inference algorithm to infer an infinite tower of options.

Dave

This is done now, yes?

No, not done yet.

So, I... can't actually reproduce this. For example, I tried Paul's example from #602 and it correctly prints a type error. I tried a version of Dave's example above, and the result is the same. Maybe something with how tags are handled has been changed recently so that this case just never happens in the unifier? I was going to fix it, but with no test case, I'm going to close it instead (reopen if you have a test case!)

Occurs check is now implemented -- see #768 -- but there may be checks missing in places that should have them.

Auto merge of rust-lang#229 - kamalmarhubi:mount-flags, r=alexcrichton

Introduce enzyme_iter for preserving approximation levels through dif…

Merge pull request rust-lang#229 from rust-lang/fix/fmaddsub

Add an __VERIFIER_expected_fail() intrinsic, and use it in a test (ru…

Parallelize & Partition Verification (rust-lang#229)

Improve `u16::carrying_mul` harness performance (rust-lang#230)

Add missing line separator (rust-lang#232)

Auto merge of rust-lang#137022 - jieyouxu:bump-bootstrap-cc-cmake, r=…

Add queue data structure (rust-lang#229)

Navigation Menu

Repository navigation

Implement the occurs check for type unification #229

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Implement the occurs check for type unification #229

Description

Activity

dherman commented on Feb 18, 2011

graydon commented on May 26, 2011

pcwalton commented on May 26, 2011

catamorphism commented on Jul 20, 2011

catamorphism commented on Aug 4, 2011

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions