Merge pull request #106 from scalexm/master

Fix `InferenceTable::normalize_lifetime`

Author: nikomatsakis

chalk-engine/src/lib.rs

@@ -49,15 +49,12 @@
 //! - HH: Hereditary harrop predicates. What Chalk deals in.
 //!   Popularized by Lambda Prolog.
 
-#![feature(conservative_impl_trait)]
 #![feature(crate_in_paths)]
 #![feature(crate_visibility_modifier)]
 #![feature(dyn_trait)]
 #![feature(in_band_lifetimes)]
-#![feature(match_default_bindings)]
 #![feature(macro_vis_matcher)]
 #![feature(step_trait)]
-#![feature(universal_impl_trait)]
 #![feature(underscore_lifetimes)]
 
 #[macro_use] extern crate chalk_macros;

src/lib.rs

@@ -1,18 +1,15 @@
 #![recursion_limit = "1024"]
 #![cfg_attr(test, feature(test))]
-#![feature(conservative_impl_trait)]
 #![feature(catch_expr)]
 #![feature(crate_in_paths)]
 #![feature(crate_visibility_modifier)]
 #![feature(dyn_trait)]
 #![feature(in_band_lifetimes)]
 #![feature(macro_at_most_once_rep)]
 #![feature(macro_vis_matcher)]
-#![feature(match_default_bindings)]
 #![feature(specialization)]
 #![feature(step_trait)]
 #![feature(underscore_lifetimes)]
-#![feature(universal_impl_trait)]
 
 extern crate chalk_parse;
 #[macro_use]

src/solve/infer/mod.rs

@@ -164,7 +164,10 @@ impl InferenceTable {
     crate fn normalize_lifetime(&mut self, leaf: &Lifetime, binders: usize) -> Option<Lifetime> {
         match *leaf {
             Lifetime::Var(v) => {
-                let v1 = self.probe_lifetime_var(InferenceVariable::from_depth(v))?;
+                if v < binders {
+                    return None;
+                }
+                let v1 = self.probe_lifetime_var(InferenceVariable::from_depth(v - binders))?;
                 Some(v1.up_shift(binders))
             }
             Lifetime::ForAll(_) => None,

src/solve/test/mod.rs

@@ -1992,3 +1992,28 @@ fn clauses_in_if_goals() {
         }
     }
 }
+
+#[test]
+fn quantified_types() {
+    test! {
+        program {
+            trait Foo { }
+            struct fn<'a> { }
+            impl Foo for for<'a> fn<'a> { }
+        }
+
+        goal {
+            for<'a> fn<'a>: Foo
+        } yields {
+            "Unique"
+        }
+
+        goal {
+            forall<'a> { fn<'a>: Foo }
+        } yields {
+            // Lifetime constraints are unsatisfiable
+            "Unique; substitution [], \
+            lifetime constraints [InEnvironment { environment: Env([]), goal: '!2 == '!1 }]"
+        }
+    }
+}