Implement the UnliftedDatatypes extensionwip/unlifted-data

GHC Proposal: 0265-unlifted-datatypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/265
Issues: https://gitlab.haskell.org/ghc/ghc/-/issues/19523
Implementation Details: Note [Implementation of UnliftedDatatypes]

This patch introduces the `UnliftedDatatypes` extension. When this extension is
enabled, GHC relaxes the restrictions around what result kinds are allowed in
data declarations. This allows data types for which an unlifted or
levity-polymorphic result kind is inferred.

The most significant changes are in `GHC.Tc.TyCl`, where
`Note [Implementation of UnliftedDatatypes]` describes the details of the
implementation.

Fixes #19523.

22 files changed, 275 insertions, 0 deletions

diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index cbcbefc573..d55dae5484 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -43,6 +43,7 @@ expectedGhcOnlyExtensions =
     , "FieldSelectors"
     , "OverloadedRecordDot"
     , "OverloadedRecordUpdate"
+    , "UnliftedDatatypes"
     ]
 
 expectedCabalOnlyExtensions :: [String]
diff --git a/testsuite/tests/unlifted-datatypes/Makefile b/testsuite/tests/unlifted-datatypes/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/Makefile b/testsuite/tests/unlifted-datatypes/should_compile/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
new file mode 100644
index 0000000000..443deadc1a
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataFams.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+
+module UnlDataFams where
+
+import GHC.Exts
+import GHC.Types
+
+data family F a :: UnliftedType
+
+data instance F Int = TInt
+
+data family G a :: TYPE (BoxedRep l)
+
+data instance G Int = GInt
+data instance G Bool :: UnliftedType where
+  GBool :: G Bool
+data instance G Char :: Type where
+  GChar :: G Char
+
+data family H :: Type -> UnliftedType
+data instance H Int = HInt Int
+
+type Interpret :: Bool -> Levity
+type family Interpret b where
+  Interpret True  = Lifted
+  Interpret False = Unlifted
+
+type A :: TYPE (BoxedRep (Interpret b))
+data A = MkA Int
+
+a :: A @True
+a = MkA 42
+
+-- type Interpret :: Bool -> RuntimeRep
+-- type family Interpret b where
+--   Interpret True  = BoxedRep Lifted
+--   Interpret False = BoxedRep Unlifted
+--
+-- type A :: TYPE (Interpret b)
+-- data A = MkA Int
+--
+-- data B :: TYPE (Interpret b) where
+--   MkB :: Int -> B @b
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs
new file mode 100644
index 0000000000..cef48e31e0
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataMonoSigs.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTSyntax #-}
+{-# LANGUAGE KindSignatures #-}
+
+module UnlDataMonoSigs where
+
+import GHC.Exts
+import GHC.Types
+
+data T1 a :: UnliftedType where
+  MkT1 :: T1 a
+
+type T2 :: Type -> UnliftedType
+data T2 a = T2
+
+type T3 :: Type -> UnliftedType
+data T3 a where
+  MkT3 :: T3 a
+
+type T4 :: Type -> UnliftedType
+data T4 a :: UnliftedType where
+  MkT4 :: T4 a
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs
new file mode 100644
index 0000000000..6e998155bf
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataPolySigs.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+
+module UnlDataPolySigs where
+
+import GHC.Exts
+import GHC.Types
+
+data U1 a :: TYPE (BoxedRep l) where
+  MkU1 :: Int -> U1 a -- (MkU1 :: forall {k} (a :: k). Int -> U1 @{k} @'Lifted a)
+
+type U2 :: Type -> TYPE (BoxedRep l)
+data U2 a = MkU2 Int -- (MkU2 :: forall (l :: Levity) a. Int -> U2 @l a)
+
+type U3 :: Type -> TYPE (BoxedRep l)
+data U3 a where
+  MkU3 :: Int -> U3 a -- (MkU3 :: forall a. Int -> U3 @'Lifted a)
+
+type U4 :: Type -> TYPE (BoxedRep l)
+data U4 a :: TYPE (BoxedRep l) where
+  MkU4 :: Int -> U4 a -- (MkU4 :: forall a. Int -> U4 @'Lifted a)
+
+data U5 a :: forall l. TYPE (BoxedRep l) where
+  MkU5 :: Int -> U5 a -- (MkU5 :: forall {k} (a :: k). Int -> U5 @{k} @'Lifted a)
+
+data U6 a :: forall l. TYPE (BoxedRep l) where
+  MkU6 :: Int -> U6 a @l -- (MkU6 :: forall {k} (a :: k) (l :: Levity). Int -> U6 @{k} a @l)
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs
new file mode 100644
index 0000000000..9023093ee8
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/UnlDataUsersGuide.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE ConstraintKinds #-}
+
+module UnlDataUsersGuide where
+
+import GHC.Exts
+import GHC.Types
+
+data UList a :: UnliftedType where
+  UCons :: a -> UList a -> UList a
+  UNil :: UList a
+
+type UList2 :: Type -> UnliftedType
+data UList2 a = UCons2 a (UList2 a) | UNil2
+
+type PEither :: Type -> Type -> TYPE (BoxedRep l)
+data PEither l r = PLeft l | PRight r
+
+f :: PEither @Unlifted Int Bool -> Bool
+f (PRight b) = b
+f _          = False
+
+type T :: TYPE (BoxedRep l)
+data T where
+  MkT :: forall l. (() :: Constraint) => T @l
+  MkT2 :: Proxy# () -> T @l
+
+t1 :: T @Lifted
+t1 = MkT
+
+t2 :: T @Lifted
+t2 = MkT2 proxy#
diff --git a/testsuite/tests/unlifted-datatypes/should_compile/all.T b/testsuite/tests/unlifted-datatypes/should_compile/all.T
new file mode 100644
index 0000000000..d8c3eeb457
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_compile/all.T
@@ -0,0 +1,4 @@
+test('UnlDataMonoSigs', normal, compile, [''])
+test('UnlDataPolySigs', normal, compile, [''])
+test('UnlDataFams', normal, compile, [''])
+test('UnlDataUsersGuide', normal, compile, [''])
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/Makefile b/testsuite/tests/unlifted-datatypes/should_fail/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs
new file mode 100644
index 0000000000..18dcd1a216
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+
+module UnlDataInvalidResKind1 where
+
+import GHC.Exts
+import GHC.Types
+
+type T :: Type -> TYPE IntRep
+data T a = MkT Int
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr
new file mode 100644
index 0000000000..e61b6b4b18
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind1.stderr
@@ -0,0 +1,4 @@
+
+UnlDataInvalidResKind1.hs:9:1: error:
+    • Data type has non-'BoxedRep return kind ‘TYPE 'IntRep’
+    • In the data declaration for ‘T’
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs
new file mode 100644
index 0000000000..427e41bf0c
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataInvalidResKind2.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+
+module UnlDataInvalidResKind2 where
+
+import GHC.Exts
+import GHC.Types
+
+type Interpret :: Bool -> RuntimeRep
+type family Interpret b = r | r -> b where
+  Interpret True  = BoxedRep Lifted
+  Interpret False = BoxedRep Unlifted
+
+-- Not allowed, although well-typed after type fam reduction
+type A :: TYPE (Interpret b)
+data A = MkA Int
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs
new file mode 100644
index 0000000000..1b59bdf24f
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE PolyKinds #-}
+
+module UnlDataNullaryPoly where
+
+import GHC.Exts
+import GHC.Types
+
+type T :: TYPE (BoxedRep l)
+data T = MkT -- Not OK, we get (MkT :: forall l. T @l :: TYPE (BoxedRep l)) which is ill-kinded.
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr
new file mode 100644
index 0000000000..7c9b856677
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/UnlDataNullaryPoly.stderr
@@ -0,0 +1,7 @@
+
+UnlDataNullaryPoly.hs:10:10: error:
+    • Quantified type's kind mentions quantified type variable
+        type: ‘forall (l :: Levity). T’
+      where the body of the forall has this kind: ‘TYPE ('BoxedRep l)’
+    • In the definition of data constructor ‘MkT’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/unlifted-datatypes/should_fail/all.T b/testsuite/tests/unlifted-datatypes/should_fail/all.T
new file mode 100644
index 0000000000..f8e8c7c833
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_fail/all.T
@@ -0,0 +1,2 @@
+test('UnlDataNullaryPoly', normal, compile_fail, [''])
+test('UnlDataInvalidResKind1', normal, compile_fail, [''])
diff --git a/testsuite/tests/unlifted-datatypes/should_run/Makefile b/testsuite/tests/unlifted-datatypes/should_run/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs
new file mode 100644
index 0000000000..19266ea71e
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+
+import GHC.Exts
+import GHC.Types
+
+type SList :: Type -> UnliftedType
+data SList a = Cons a (SList a) | Nil
+
+-- Sadly no IsList (SList a) or Show a => Show (SList a),
+-- because type classes require lifted rep
+sfromList :: [a] -> SList a
+sfromList []     = Nil
+sfromList (x:xs) = Cons x (sfromList xs)
+stoList :: SList a -> [a]
+stoList (Cons x xs) = x:stoList xs
+stoList Nil         = []
+
+sfromList2 :: [a] -> SList a
+sfromList2 xs = foldl (\acc x xs -> acc (Cons x xs)) (\x -> x) xs Nil
+
+sfromList3 :: [a] -> SList a
+sfromList3 xs = foldr (\x acc xs -> Cons x (acc xs)) (\x -> x) xs Nil
+
+sreverse :: SList a -> SList a
+sreverse = go Nil
+  where
+    go acc Nil         = acc
+    go acc (Cons x xs) = go (Cons x acc) xs
+
+main = do
+  print (stoList (sreverse (Cons 1 (Cons 2 (Cons 3 Nil)))))
+  print (stoList (sreverse (sfromList [2,3,4])))
+  print (stoList (sreverse (sfromList2 [3,4,5])))
+  print (stoList (sreverse (sfromList3 [4,5,6])))
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout
new file mode 100644
index 0000000000..0b1c480e31
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlData1.stdout
@@ -0,0 +1,4 @@
+[3,2,1]
+[4,3,2]
+[5,4,3]
+[6,5,4]
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs
new file mode 100644
index 0000000000..ed19c3236f
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE UnliftedDatatypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+
+import GHC.Exts
+import GHC.Types
+
+data T a :: UnliftedType where
+  TInt :: T Int
+
+f :: T a -> Int
+f _ = 0
+
+g :: T a -> T a
+g TInt = TInt
+{-# NOINLINE g #-}
+
+main = do
+  case g TInt of TInt -> putStrLn "should see this"
+  print (f (error "boom")) -- crashes!
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr
new file mode 100644
index 0000000000..158e2a12ba
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stderr
@@ -0,0 +1,3 @@
+UnlGadt1: boom
+CallStack (from HasCallStack):
+  error, called at UnlGadt1.hs:19:13 in main:Main
diff --git a/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout
new file mode 100644
index 0000000000..b31e365734
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/UnlGadt1.stdout
@@ -0,0 +1 @@
+should see this
diff --git a/testsuite/tests/unlifted-datatypes/should_run/all.T b/testsuite/tests/unlifted-datatypes/should_run/all.T
new file mode 100644
index 0000000000..87b69c89bf
--- /dev/null
+++ b/testsuite/tests/unlifted-datatypes/should_run/all.T
@@ -0,0 +1,2 @@
+test('UnlData1', normal, compile_and_run, [''])
+test('UnlGadt1', exit_code(1), compile_and_run, [''])