use Cons for Wcs too

It's clearer to read

Author: nikomatsakis

crates/formality-core/src/collections.rs

@@ -156,6 +156,7 @@ tuple_upcast!(Vec: A, B, C, D);
 /// where `head` will be the first item in the collection
 /// and tail will be a collection with the remaining items.
 /// Both can also be downcast to `()` which matches an empty collection.
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct Cons<T, C>(pub T, pub C);
 
 impl<T> DowncastTo<Cons<T, Set<T>>> for Set<T>

crates/formality-core/src/lib.rs

@@ -37,6 +37,7 @@ pub mod variable;
 pub mod visit;
 
 pub use cast::{Downcast, DowncastFrom, DowncastTo, Downcasted, To, Upcast, UpcastFrom, Upcasted};
+pub use collections::Cons;
 pub use collections::Deduplicate;
 pub use collections::Map;
 pub use collections::Set;

crates/formality-prove/src/prove/prove_wc_list.rs

@@ -1,4 +1,4 @@
-use formality_core::judgment_fn;
+use formality_core::{judgment_fn, Cons};
 use formality_types::grammar::Wcs;
 
 use crate::{
@@ -28,7 +28,7 @@ judgment_fn! {
             (prove_wc(&decls, env, &assumptions, wc0) => c)
             (prove_after(&decls, c, &assumptions, &wcs1) => c)
             --- ("some")
-            (prove_wc_list(decls, env, assumptions, (wc0, wcs1)) => c)
+            (prove_wc_list(decls, env, assumptions, Cons(wc0, wcs1)) => c)
         )
     }
 }

crates/formality-types/src/grammar/wc.rs

@@ -1,7 +1,7 @@
 use std::sync::Arc;
 
 use formality_core::{
-    cast_impl, set, term, DowncastFrom, DowncastTo, Set, SetExt, Upcast, UpcastFrom, Upcasted,
+    cast_impl, set, term, Cons, DowncastFrom, DowncastTo, Set, Upcast, UpcastFrom, Upcasted,
 };
 
 use crate::grammar::PR;
@@ -83,14 +83,10 @@ tuple_upcast!(A, B);
 tuple_upcast!(A, B, C);
 tuple_upcast!(A, B, C, D);
 
-impl DowncastTo<(Wc, Wcs)> for Wcs {
-    fn downcast_to(&self) -> Option<(Wc, Wcs)> {
-        if self.set.is_empty() {
-            None
-        } else {
-            let (wc, set) = self.set.clone().split_first().unwrap();
-            Some((wc, set.upcast()))
-        }
+impl DowncastTo<Cons<Wc, Wcs>> for Wcs {
+    fn downcast_to(&self) -> Option<Cons<Wc, Wcs>> {
+        let Cons(wc, set) = self.set.downcast_to()?;
+        Some(Cons(wc, set.upcast()))
     }
 }