Commit fd8b044e authored by Edward Z. Yang's avatar Edward Z. Yang Committed by Ben Gamari

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: default avatarEdward 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
parent 71a42356
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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'
......
......@@ -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 _ []
......
......@@ -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,
......
{-# 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#))
......@@ -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, [''])
......@@ -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 #)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment