add Goal::CannotProve and extract ProgramClause struct

src/librustc/ich/impls_ty.rs

@@ -1413,6 +1413,7 @@ fn hash_stable<W: StableHasherResult>(&self,
                 quantifier.hash_stable(hcx, hasher);
                 goal.hash_stable(hcx, hasher);
             },
+            CannotProve => { },
         }
     }
 }

src/librustc/traits/mod.rs

@@ -286,7 +286,8 @@ pub enum Goal<'tcx> {
     And(&'tcx Goal<'tcx>, &'tcx Goal<'tcx>),
     Not(&'tcx Goal<'tcx>),
     DomainGoal(DomainGoal<'tcx>),
-    Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>)
+    Quantified(QuantifierKind, ty::Binder<&'tcx Goal<'tcx>>),
+    CannotProve,
 }
 
 impl<'tcx> Goal<'tcx> {

src/librustc/traits/structural_impls.rs

@@ -491,6 +491,7 @@ fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
                 // FIXME: appropriate binder names
                 write!(fmt, "{}<> {{ {} }}", qkind, goal.skip_binder())
             }
+            CannotProve => write!(fmt, "CannotProve"),
         }
     }
 }
@@ -557,6 +558,7 @@ impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
         (traits::Goal::Not)(goal),
         (traits::Goal::DomainGoal)(domain_goal),
         (traits::Goal::Quantified)(qkind, goal),
+        (traits::Goal::CannotProve),
     }
 }