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

5 files changed, 44 insertions, 13 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 _ []