Simplify index unification (#448)

polarity-lang · Jan 16, 2025 · dbc8b9e · dbc8b9e
1 parent 9e3f91e
commit dbc8b9e
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 65 deletions.
diff --git a/lang/elaborator/src/index_unification/dec.rs b/lang/elaborator/src/index_unification/dec.rs
@@ -1,53 +1,17 @@
 use std::fmt;
 
-pub enum Dec<Y = (), N = ()> {
+pub enum Dec<Y = ()> {
     Yes(Y),
-    No(N),
+    No,
 }
 
 pub use Dec::*;
 
-impl<Y: fmt::Debug, N: fmt::Debug> fmt::Debug for Dec<Y, N> {
+impl<Y: fmt::Debug> fmt::Debug for Dec<Y> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
             Self::Yes(arg) => f.debug_tuple("Yes").field(arg).finish(),
-            Self::No(arg) => f.debug_tuple("No").field(arg).finish(),
-        }
-    }
-}
-
-impl<Y, N> Dec<Y, N> {
-    pub fn map_yes<F, Y2>(self, f: F) -> Dec<Y2, N>
-    where
-        F: FnOnce(Y) -> Y2,
-    {
-        match self {
-            Yes(arg) => Yes(f(arg)),
-            No(arg) => No(arg),
-        }
-    }
-
-    pub fn map_no<F, N2>(self, f: F) -> Dec<Y, N2>
-    where
-        F: FnOnce(N) -> N2,
-    {
-        match self {
-            Yes(arg) => Yes(arg),
-            No(arg) => No(f(arg)),
-        }
-    }
-
-    pub fn ok_yes(self) -> Result<Y, N> {
-        match self {
-            Yes(arg) => Ok(arg),
-            No(arg) => Err(arg),
-        }
-    }
-
-    pub fn ok_no(self) -> Result<N, Y> {
-        match self {
-            Yes(arg) => Err(arg),
-            No(arg) => Ok(arg),
+            Self::No => f.debug_tuple("No").finish(),
         }
     }
 }
diff --git a/lang/elaborator/src/index_unification/unify.rs b/lang/elaborator/src/index_unification/unify.rs
@@ -54,7 +54,7 @@ pub fn unify(
     let mut ctx = Ctx::new(vec![constraint], ctx.clone());
     let res = match ctx.unify(while_elaborating_span)? {
         Yes(_) => Yes(ctx.unif),
-        No(()) => No(()),
+        No => No,
     };
     Ok(res)
 }
@@ -81,7 +81,7 @@ impl Ctx {
                 Yes(_) => {
                     self.done.insert(constraint);
                 }
-                No(_) => return Ok(No(())),
+                No => return Ok(No),
             }
         }
 
@@ -118,7 +118,7 @@ impl Ctx {
                 (Exp::TypCtor(TypCtor { name, .. }), Exp::TypCtor(TypCtor { name: name2, .. }))
                     if name != name2 =>
                 {
-                    Ok(No(()))
+                    Ok(No)
                 }
                 (
                     Exp::Call(Call { name, args, .. }),
@@ -131,7 +131,7 @@ impl Ctx {
                 (Exp::Call(Call { name, .. }), Exp::Call(Call { name: name2, .. }))
                     if name != name2 =>
                 {
-                    Ok(No(()))
+                    Ok(No)
                 }
                 (
                     Exp::DotCall(DotCall { exp, name, args, .. }),

diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs
@@ -178,12 +178,14 @@ impl WithExpectedType<'_> {
                         // this case is really absurd. To do this, we verify that the unification
                         // actually fails.
                         None => {
-                            unify(ctx.levels(), constraint, span)?
-                                .map_yes(|_| TypeError::PatternIsNotAbsurd {
+                            let res = unify(ctx.levels(), constraint, span)?;
+                            if let crate::index_unification::dec::Dec::Yes(_) = res {
+                                let err = TypeError::PatternIsNotAbsurd {
                                     name: Box::new(name.clone()),
                                     span: span.to_miette(),
-                                })
-                                .ok_no()?;
+                                };
+                                return Err(err);
+                            }
 
                             let case_out = Case {
                                 span: *span,
@@ -297,12 +299,18 @@ impl WithExpectedType<'_> {
                                 }
                             };
                             let body_out = {
-                                let unif = unify(ctx.levels(), constraint, span)?
-                                    .map_no(|()| TypeError::PatternIsAbsurd {
-                                        name: Box::new(name.clone()),
-                                        span: span.to_miette(),
-                                    })
-                                    .ok_yes()?;
+                                let res = unify(ctx.levels(), constraint, span)?;
+                                let unif = match res {
+                                    crate::index_unification::dec::Dec::Yes(unif) => unif,
+                                    crate::index_unification::dec::Dec::No => {
+                                        // The pattern is absurd.
+                                        let err = TypeError::PatternIsAbsurd {
+                                            name: Box::new(name.clone()),
+                                            span: span.to_miette(),
+                                        };
+                                        return Err(err);
+                                    }
+                                };
 
                                 ctx.fork::<Result<_, TypeError>, _>(|ctx| {
                                     let type_info_table = ctx.type_info_table.clone();

diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs
@@ -262,12 +262,18 @@ impl WithScrutineeType<'_> {
                         Some(body) => {
                             // The programmer wrote a non-absurd case. We therefore have to check
                             // that the unification succeeds.
-                            let unif = unify(ctx.levels(), constraint, &span)?
-                                .map_no(|()| TypeError::PatternIsAbsurd {
-                                    name: Box::new(name.clone()),
-                                    span: span.to_miette(),
-                                })
-                                .ok_yes()?;
+                            let res = unify(ctx.levels(), constraint, &span)?;
+                            let unif = match res {
+                                crate::index_unification::dec::Dec::Yes(unif) => unif,
+                                crate::index_unification::dec::Dec::No => {
+                                    // A right-hand side was provided in the clause, but unification fails.
+                                    let err = TypeError::PatternIsAbsurd {
+                                        name: Box::new(name.clone()),
+                                        span: span.to_miette(),
+                                    };
+                                    return Err(err);
+                                }
+                            };
 
                             ctx.fork::<Result<_, TypeError>, _>(|ctx| {
                                 let type_info_table = ctx.type_info_table.clone();
@@ -287,13 +293,15 @@ impl WithScrutineeType<'_> {
                             // The programmer wrote an absurd case. We therefore have to check whether
                             // this case is really absurd. To do this, we verify that the unification
                             // actually fails.
-                            unify(ctx.levels(), constraint, &span)?
-                                .map_yes(|_| TypeError::PatternIsNotAbsurd {
+                            let res = unify(ctx.levels(), constraint, &span)?;
+                            if let crate::index_unification::dec::Dec::Yes(_) = res {
+                                // The case was annotated as absurd but index unification succeeds.
+                                let err = TypeError::PatternIsNotAbsurd {
                                     name: Box::new(name.clone()),
                                     span: span.to_miette(),
-                                })
-                                .ok_no()?;
-
+                                };
+                                return Err(err);
+                            }
                             None
                         }
                     };