remove the blanket impl of UpcastFrom<()>

This was kind of surprising.

Author: nikomatsakis

crates/formality-core/src/cast.rs

@@ -232,12 +232,9 @@ impl DowncastTo<()> for () {
     }
 }
 
-impl<T> UpcastFrom<()> for T
-where
-    T: Default,
-{
+impl UpcastFrom<()> for () {
     fn upcast_from((): ()) -> Self {
-        Default::default()
+        ()
     }
 }
 

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

@@ -1,4 +1,4 @@
-use formality_core::{cast_impl, visit::CoreVisit, Set, To, Upcast};
+use formality_core::{cast_impl, visit::CoreVisit, Set, To, Upcast, UpcastFrom};
 use formality_macros::term;
 use formality_types::{
     grammar::{
@@ -232,3 +232,9 @@ impl CoreVisit<crate::FormalityLang> for Env {
         assert_eq!(s.len(), self.variables.len());
     }
 }
+
+impl UpcastFrom<()> for Env {
+    fn upcast_from((): ()) -> Self {
+        Env::default()
+    }
+}

crates/formality-prove/src/test/adt_wf.rs

@@ -5,7 +5,7 @@ use formality_types::{
     rust::term,
 };
 
-use crate::{decls::Decls, prove::prove};
+use crate::{decls::Decls, prove::prove, Env};
 
 fn decls() -> Decls {
     Decls {
@@ -20,7 +20,12 @@ fn decls() -> Decls {
 fn well_formed_adt() {
     let assumptions: Wcs = Wcs::t();
     let goal: Parameter = term("X<u32>");
-    let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal));
+    let constraints = prove(
+        decls(),
+        Env::default(),
+        assumptions,
+        Relation::WellFormed(goal),
+    );
     expect![[r#"
         {
             Constraints {
@@ -40,7 +45,12 @@ fn well_formed_adt() {
 fn not_well_formed_adt() {
     let assumptions: Wcs = Wcs::t();
     let goal: Parameter = term("X<u64>");
-    let constraints = prove(decls(), (), assumptions, Relation::WellFormed(goal));
+    let constraints = prove(
+        decls(),
+        Env::default(),
+        assumptions,
+        Relation::WellFormed(goal),
+    );
     expect![[r#"
         {}
     "#]]

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

@@ -94,6 +94,12 @@ impl DowncastTo<(Wc, Wcs)> for Wcs {
     }
 }
 
+impl UpcastFrom<()> for Wcs {
+    fn upcast_from((): ()) -> Self {
+        Wcs::default()
+    }
+}
+
 impl DowncastTo<()> for Wcs {
     fn downcast_to(&self) -> Option<()> {
         if self.set.is_empty() {