lude

commit b0e23b53beb3c1aa813beef938bdd30842dcf866
parent 49af51c87b8fd1dde1b2ac6f08b04248b9c7b4db
Author: Robert Russell <robert@rr3.xyz>
Date:   Fri,  4 Sep 2026 20:52:41 -0700

Generalize deduce

Diffstat:
M
src/Lude/Constraint/Evidence.hs
 | 
27
++++++++++++---------------

1 file changed, 12 insertions(+), 15 deletions(-)
diff --git a/src/Lude/Constraint/Evidence.hs b/src/Lude/Constraint/Evidence.hs
@@ -1,14 +1,14 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Lude.Constraint.Evidence (
-    deduce,
     Witness,
     Witnesses (..),
     (:=>),
-    tautology,
     consider,
+    tautology,
     because,
     (\\),
+    deduce,
 ) where
 
 import Lude.Constraint.Core
@@ -17,15 +17,7 @@ import Lude.Kind
 --------------------------------------------------------------------------------
 
 infixr 1 :=>
-infixl 4 \\
-
---------------------------------------------------------------------------------
-
--- TODO: Can we replace deduce with consider?
-
--- | Given that `a` implies `b`, deduce evidence of `b` from evidence of `a`
-deduce :: ((a) => b) => Evidence a -> Evidence b
-deduce Evidence = Evidence
+infixl 1 \\
 
 --------------------------------------------------------------------------------
 -- Witnesses
@@ -45,21 +37,26 @@ class Witnesses a b where
 type (:=>) :: Relation Type Constraint
 type (:=>) = Canonically Witnesses
 
-tautology :: forall a b. (b) => Witness a b
-tautology _ = Evidence
-
 -- | Witness the canonical conclusion `b` of `a`
 --
 -- Unlike `witness`, `a` determines `b`, so we don't require a type argument.
 consider :: forall a b. (a :=> b) => Witness a b
 consider = witness b
 
+tautology :: forall a b. (b) => Witness a b
+tautology _ = Evidence
+
 -- | Given that `a` (canonically) witnesses `c`, resolve a `c`-predicated
 -- `b` with an `a`
-because, (\\) :: forall a b c. (a :=> c) => ((c) => b) -> a -> b
+because, (\\) :: forall b a c. (a :=> c) => ((c) => b) -> a -> b
 b `because` a = case consider a of Evidence -> b
 (\\) = because
 
+-- | Given that `a` (canonically) witnesses `b` and `b` implies `c`, we know
+-- that `a` witnesses `c`
+deduce :: forall c a b. (a :=> b, (b) => c) => Witness a c
+deduce = (Evidence \\)
+
 --------------------------------------------------------------------------------
 -- Instances