lude

commit 58d2f9ac80fefbdc09a6cea101a4f1fdc5c6af13
parent bdc0d4814d4dfdf2603a407e42cd522ce45906d4
Author: Robert Russell <robert@rr3.xyz>
Date:   Sat,  3 Oct 2026 20:12:10 -0700

Haskell: add Brand and OpenKind

Diffstat:
M
src/Lude/Haskell/Core.hs
 | 
29
++++++++++++++++++++++++++++-
M
src/Lude/Haskell/Defunctionalization.hs
 | 
7
++-----

2 files changed, 30 insertions(+), 6 deletions(-)
diff --git a/src/Lude/Haskell/Core.hs b/src/Lude/Haskell/Core.hs
@@ -3,6 +3,8 @@ module Lude.Haskell.Core (
     KindOrType#,
     KindOrType,
     Kind,
+    Brand,
+    OpenKind,
     Endo,
     Biendo,
 ) where
@@ -11,7 +13,7 @@ import GHC.Exts qualified as GHC
 
 --------------------------------------------------------------------------------
 
--- This is just so "kind-level primitives" (@Kind@, @Repr@, etc.) receive a
+-- | This is just so "kind-level primitives" (@Kind@, @Repr@, etc.) receive a
 -- valid Lude signature in GHC diagnostic messages
 type KIND = GHC.TYPE GHC.LiftedRep
 
@@ -30,6 +32,31 @@ type KindOrType = KindOrType# GHC.LiftedRep
 type Kind :: KIND
 type Kind = KindOrType
 
+-- | The kind of brands for `OpenKind`
+type Brand :: KIND
+type Brand = Kind
+
+-- | Open (i.e., extensible) kinds, which have a brand to distinguish different
+-- open kinds
+--
+-- Example usage:
+-- @
+-- data FooBrand :: Brand
+-- type FooKind = OpenKind FooBrand
+-- data FooA :: FooKind       -- Nullary FooKind constructor
+-- data FooB :: X -> FooKind  -- Unary FooKind constructor
+-- -- ...
+-- @
+--
+-- Open kinds can also have arguments:
+-- @
+-- data BarBrand :: X -> Brand
+-- type BarKind x = OpenKind (BarBrand x)
+-- -- ...
+-- @
+type OpenKind :: Brand -> Kind
+type OpenKind b = b -> Kind
+
 type Endo :: forall (r :: Repr). KindOrType# r -> KindOrType
 type Endo i = i -> i
 
diff --git a/src/Lude/Haskell/Defunctionalization.hs b/src/Lude/Haskell/Defunctionalization.hs
@@ -11,13 +11,10 @@ import Lude.Haskell.Core
 
 --------------------------------------------------------------------------------
 
--- | An empty kind with a phantom kind index, used to make @T k@ opaque
-type T' :: Kind -> Kind
-data T' k
+data TBrand :: Kind -> Brand
 
 -- | A type expression (of a given kind)
-type T :: Kind -> Kind
-type T k = T' k -> Kind
+type T k = OpenKind (TBrand k)
 
 type Splice :: forall {k}. T k -> k
 type family Splice _