Levity polymorphic Backpack.

This patch makes it possible to specify non * kinds of
abstract data types in signatures, so you can have
levity polymorphism through Backpack, without the runtime
representation constraint!

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: andrewthad, bgamari, austin, goldfire

Reviewed By: bgamari

Subscribers: goldfire, rwbarton, thomie

GHC Trac Issues: #13955

Differential Revision: https://phabricator.haskell.org/D3825

10 files changed, 107 insertions, 16 deletions

diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs
index 296b4e2f3c..2199965d13 100644
--- a/compiler/backpack/RnModIface.hs
+++ b/compiler/backpack/RnModIface.hs
@@ -424,11 +424,13 @@ rnIfaceDecl d@IfaceData{} = do
             binders <- mapM rnIfaceTyConBinder (ifBinders d)
             ctxt <- mapM rnIfaceType (ifCtxt d)
             cons <- rnIfaceConDecls (ifCons d)
+            res_kind <- rnIfaceType (ifResKind d)
             parent <- rnIfaceTyConParent (ifParent d)
             return d { ifName = name
                      , ifBinders = binders
                      , ifCtxt = ctxt
                      , ifCons = cons
+                     , ifResKind = res_kind
                      , ifParent = parent
                      }
 rnIfaceDecl d@IfaceSynonym{} = do
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 885e119abc..ed96d33826 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -700,18 +700,18 @@ pprIfaceDecl :: ShowSub -> IfaceDecl -> SDoc
 -- NB: pprIfaceDecl is also used for pretty-printing TyThings in GHCi
 --     See Note [Pretty-printing TyThings] in PprTyThing
 pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
-                             ifCtxt = context,
+                             ifCtxt = context, ifResKind = kind,
                              ifRoles = roles, ifCons = condecls,
                              ifParent = parent,
                              ifGadtSyntax = gadt,
                              ifBinders = binders })
 
   | gadt      = vcat [ pp_roles
-                     , pp_nd <+> pp_lhs <+> pp_where
+                     , pp_nd <+> pp_lhs <+> pp_kind <+> pp_where
                      , nest 2 (vcat pp_cons)
                      , nest 2 $ ppShowIface ss pp_extra ]
   | otherwise = vcat [ pp_roles
-                     , hang (pp_nd <+> pp_lhs) 2 (add_bars pp_cons)
+                     , hang (pp_nd <+> pp_lhs <+> pp_kind) 2 (add_bars pp_cons)
                      , nest 2 $ ppShowIface ss pp_extra ]
   where
     is_data_instance = isIfaceDataInstance parent
@@ -719,6 +719,9 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     cons       = visibleIfConDecls condecls
     pp_where   = ppWhen (gadt && not (null cons)) $ text "where"
     pp_cons    = ppr_trim (map show_con cons) :: [SDoc]
+    pp_kind
+      | isIfaceLiftedTypeKind kind = empty
+      | otherwise = dcolon <+> ppr kind
 
     pp_lhs = case parent of
                IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index fbfd017f23..e5a07ec99e 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -23,6 +23,7 @@ module TcHsType (
                 -- Type checking type and class decls
         kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
         tcDataKindSig,
+        DataKindCheck(..),
 
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
@@ -1900,7 +1901,18 @@ tcTyClTyVars tycon_name thing_inside
 
 
 -----------------------------------
-tcDataKindSig :: Bool  -- ^ Do we require the result to be *?
+data DataKindCheck
+    -- Plain old data type; better be lifted
+    = LiftedDataKind
+    -- Data families might have a variable return kind.
+    -- See See Note [Arity of data families] in FamInstEnv for more info.
+    | LiftedOrVarDataKind
+    -- Abstract data in hsig files can have any kind at all;
+    -- even unlifted. This is because they might not actually
+    -- be implemented with a data declaration at the end of the day.
+    | AnyDataKind
+
+tcDataKindSig :: DataKindCheck  -- ^ Do we require the result to be *?
               -> Kind -> TcM ([TyConBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
 --      e.g.  data T :: * -> * -> * where ...
@@ -1912,10 +1924,15 @@ tcDataKindSig :: Bool  -- ^ Do we require the result to be *?
 -- Never emits constraints.
 -- Returns the new TyVars, the extracted TyBinders, and the new, reduced
 -- result kind (which should always be Type or a synonym thereof)
-tcDataKindSig check_for_type kind
-  = do  { checkTc (isLiftedTypeKind res_kind || (not check_for_type &&
-                                                 isJust (tcGetCastedTyVar_maybe res_kind)))
-                  (badKindSig check_for_type kind)
+tcDataKindSig kind_check kind
+  = do  { case kind_check of
+            LiftedDataKind ->
+                checkTc (isLiftedTypeKind res_kind)
+                        (badKindSig True kind)
+            LiftedOrVarDataKind ->
+                checkTc (isLiftedTypeKind res_kind || isJust (tcGetCastedTyVar_maybe res_kind))
+                        (badKindSig False kind)
+            AnyDataKind -> return ()
         ; span <- getSrcSpanM
         ; us   <- newUniqueSupply
         ; rdr_env <- getLocalRdrEnv
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 4c992e11c7..89a0ec6272 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -669,7 +669,7 @@ tcDataFamInstDecl mb_clsinfo
 
          -- Deal with any kind signature.
          -- See also Note [Arity of data families] in FamInstEnv
-       ; (extra_tcbs, final_res_kind) <- tcDataKindSig True res_kind'
+       ; (extra_tcbs, final_res_kind) <- tcDataKindSig LiftedDataKind res_kind'
 
        ; let (eta_pats, etad_tvs) = eta_reduce pats'
              eta_tvs              = filterOut (`elem` etad_tvs) tvs'
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 58a45a954b..89fbca53e6 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -831,7 +831,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
   = tcTyClTyVars tc_name $ \ binders res_kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; (extra_binders, real_res_kind) <- tcDataKindSig False res_kind
+  ; (extra_binders, real_res_kind) <- tcDataKindSig LiftedOrVarDataKind res_kind
   ; tc_rep_name <- newTyConRepName tc_name
   ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                               real_res_kind
@@ -976,7 +976,12 @@ tcDataDefn roles_info
          (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                      , dd_ctxt = ctxt, dd_kindSig = mb_ksig
                      , dd_cons = cons })
- =  do { (extra_bndrs, real_res_kind) <- tcDataKindSig True res_kind
+ =  do { tcg_env         <- getGblEnv
+       ; let hsc_src = tcg_src tcg_env
+             check_kind = if mk_permissive_kind hsc_src cons
+                            then AnyDataKind
+                            else LiftedDataKind
+       ; (extra_bndrs, real_res_kind) <- tcDataKindSig check_kind res_kind
        ; let final_bndrs  = tycon_binders `chkAppend` extra_bndrs
              roles        = roles_info tc_name
 
@@ -984,8 +989,6 @@ tcDataDefn roles_info
        ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv
                                               stupid_tc_theta
        ; kind_signatures <- xoptM LangExt.KindSignatures
-       ; tcg_env         <- getGblEnv
-       ; let hsc_src = tcg_src tcg_env
 
              -- Check that we don't use kind signatures without Glasgow extensions
        ; when (isJust mb_ksig) $
@@ -1009,6 +1012,12 @@ tcDataDefn roles_info
        ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
        ; return tycon }
   where
+    -- Abstract data types in hsig files can have arbitrary kinds,
+    -- because they may be implemented by type synonyms
+    -- (which themselves can have arbitrary kinds, not just *)
+    mk_permissive_kind HsigFile [] = True
+    mk_permissive_kind _ _ = False
+
     -- In hs-boot, a 'data' declaration with no constructors
     -- indicates a nominally distinct abstract data type.
     mk_tc_rhs HsBootFile _ []
diff --git a/docs/users_guide/separate_compilation.rst b/docs/users_guide/separate_compilation.rst
index 0de5eb59cd..10ae28cbcc 100644
--- a/docs/users_guide/separate_compilation.rst
+++ b/docs/users_guide/separate_compilation.rst
@@ -998,7 +998,18 @@ to ``hs-boot`` files, but with some slight changes:
 
   If you do not write out the constructors, you may need to give a kind to tell
   GHC what the kinds of the type variables are, if they are not the default
-  ``*``.
+  ``*``.  Unlike regular data type declarations, the return kind of an
+  abstract data declaration can be anything (in which case it probably
+  will be implemented using a type synonym.)  This can be used
+  to allow compile-time representation polymorphism (as opposed to
+  `run-time representation polymorphism <#runtime-rep>`__),
+  as in this example::
+
+        signature Number where
+            import GHC.Types
+            data Rep :: RuntimeRep
+            data Number :: TYPE Rep
+            plus :: Number -> Number -> Number
 
   Roles of type parameters are subject to the subtyping
   relation ``phantom < representational < nominal``: for example,
diff --git a/testsuite/tests/backpack/should_run/T13955.bkp b/testsuite/tests/backpack/should_run/T13955.bkp
new file mode 100644
index 0000000000..a7d447f169
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T13955.bkp
@@ -0,0 +1,44 @@
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+
+unit number-unknown where
+  signature NumberUnknown where
+    import GHC.Types
+    data Rep :: RuntimeRep
+    data Number :: TYPE Rep
+    plus :: Number -> Number -> Number
+    multiply :: Number -> Number -> Number
+  module NumberStuff where
+    import NumberUnknown
+    funcA :: Number -> Number -> Number
+    funcA x y = plus x (multiply x y)
+
+unit number-int where
+  module NumberUnknown where
+    import GHC.Types
+    type Rep = LiftedRep
+    type Number = Int
+    plus :: Int -> Int -> Int
+    plus = (+)
+    multiply :: Int -> Int -> Int
+    multiply = (*)
+
+unit number-unboxed-int where
+  module NumberUnknown where
+    import GHC.Types
+    import GHC.Prim
+    type Rep = IntRep
+    type Number = Int#
+    plus :: Int# -> Int# -> Int#
+    plus = (+#)
+    multiply :: Int# -> Int# -> Int#
+    multiply = (*#)
+
+unit main where
+  dependency number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown]
+  module Main where
+    import NumberStuff
+    import GHC.Types
+    main = print (I# (funcA 2# 3#))
diff --git a/testsuite/tests/backpack/should_run/T13955.stdout b/testsuite/tests/backpack/should_run/T13955.stdout
new file mode 100644
index 0000000000..45a4fb75db
--- /dev/null
+++ b/testsuite/tests/backpack/should_run/T13955.stdout
@@ -0,0 +1 @@
+8
diff --git a/testsuite/tests/backpack/should_run/all.T b/testsuite/tests/backpack/should_run/all.T
index b32560059b..436e142e4d 100644
--- a/testsuite/tests/backpack/should_run/all.T
+++ b/testsuite/tests/backpack/should_run/all.T
@@ -6,3 +6,4 @@ test('bkprun05', exit_code(1), backpack_run, [''])
 test('bkprun06', normal, backpack_run, [''])
 test('bkprun07', normal, backpack_run, [''])
 test('bkprun08', normal, backpack_run, [''])
+test('T13955', normal, backpack_run, [''])
diff --git a/testsuite/tests/ghci/scripts/T7627.stdout b/testsuite/tests/ghci/scripts/T7627.stdout
index ff4e67005e..8bf93a0d0f 100644
--- a/testsuite/tests/ghci/scripts/T7627.stdout
+++ b/testsuite/tests/ghci/scripts/T7627.stdout
@@ -7,7 +7,8 @@ instance Show () -- Defined in ‘GHC.Show’
 instance Read () -- Defined in ‘GHC.Read’
 instance Enum () -- Defined in ‘GHC.Enum’
 instance Bounded () -- Defined in ‘GHC.Enum’
-data (##) = (##) 	-- Defined in ‘GHC.Prim’
+data (##) :: TYPE ('GHC.Types.TupleRep '[]) = (##)
+  	-- Defined in ‘GHC.Prim’
 () :: ()
 (##) :: (# #)
 (   ) :: ()
@@ -28,7 +29,9 @@ instance Foldable ((,) a) -- Defined in ‘Data.Foldable’
 instance Traversable ((,) a) -- Defined in ‘Data.Traversable’
 instance (Bounded a, Bounded b) => Bounded (a, b)
   -- Defined in ‘GHC.Enum’
-data (#,#) (a :: TYPE k0) (b :: TYPE k1) = (#,#) a b
+data (#,#) (a :: TYPE k0) (b :: TYPE k1) :: TYPE
+                                              ('GHC.Types.TupleRep '[k0, k1])
+  = (#,#) a b
   	-- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
 (#,#) :: a -> b -> (# a, b #)