lude

commit 3cd23ca31e78d63bd546da77b2ef3c8c35e45361
parent 11b20c31df8d2175b81403b0cf5fd71eb622155b
Author: Robert Russell <robert@rr3.xyz>
Date:   Wed, 14 Oct 2026 21:15:49 -0700

Haskell.Functional: add coercion stuff

Diffstat:
M
src/Lude/Haskell/Functional.hs
 | 
8
++++++++

1 file changed, 8 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Haskell/Functional.hs b/src/Lude/Haskell/Functional.hs
@@ -1,13 +1,17 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 
 module Lude.Haskell.Functional (
     Lev,
+    coerceLev,
     Functional# (..),
+    Box(..), -- Make constructors visible for coercions.
     ($#),
     lam2#,
     app2#,
 ) where
 
+import Data.Coerce
 import Data.Tuple.Experimental qualified as GHC
 
 import Lude.Haskell.Constraint
@@ -31,6 +35,10 @@ import Lude.Haskell.Type
 type Lev :: forall {r :: Repr}. Type# r -> Type
 type Lev a = (GHC.CTuple0) => a
 
+-- | Coerce between levitated types
+coerceLev :: forall {r :: Repr} (a :: Type# r) (b :: Type# r). (Coercible a b) => Lev a -> Lev b
+coerceLev = coerce @(Lev a) @(Lev b)
+
 type Functional# :: Repr -> Constraint
 class Functional# r where
     data Box :: Type# r -> Type