lude

commit 30e2a05ed2f7075551fd0811a5e3a1126ad1bbcd
parent dff6da1a5d97c948f8ea1ed43a9b92232ab2fde4
Author: Robert Russell <robert@rr3.xyz>
Date:   Tue, 10 Mar 2026 20:41:14 -0700

Reexport equality types

Diffstat:
M
package.yaml
 | 
1
+
M
src/Lude/Kind.hs
 | 
15
+++++----------

2 files changed, 6 insertions(+), 10 deletions(-)
diff --git a/package.yaml b/package.yaml
@@ -35,6 +35,7 @@ default-extensions:
     - NoImplicitPrelude
     - OverloadedStrings
     - PatternSynonyms
+    - QuantifiedConstraints
     - TypeAbstractions
     - TypeData
     - TypeFamilies
diff --git a/src/Lude/Kind.hs b/src/Lude/Kind.hs
@@ -1,7 +1,9 @@
 module Lude.Kind (
     Kind,
-    Fst,
-    Snd,
+    (:~:) (..),
+    (:~~:) (..),
+    type (~),
+    type (~~),
     Type,
     TypeL,
     TypeU,
@@ -11,6 +13,7 @@ module Lude.Kind (
     Lev,
 ) where
 
+import Data.Type.Equality ((:~:) (..), (:~~:) (..), type (~), type (~~))
 import GHC.Exts qualified as GHC
 
 import Lude.Repr (Repr)
@@ -22,14 +25,6 @@ type Kind = GHC.TYPE Repr.BoxL
 
 --------------------------------------------------------------------------------
 
-type family Fst (p :: (i, j)) :: i where
-    Fst '(a, b) = a
-
-type family Snd (p :: (i, j)) :: j where
-    Snd '(a, b) = b
-
---------------------------------------------------------------------------------
-
 type Type :: forall (r :: Repr). Kind
 type Type @r = GHC.TYPE r