Opened 15 months ago
Closed 11 months ago
#13955 closed feature request (fixed)
Backpack does not handle unlifted types
Reported by: | andrewthad | Owned by: | |
---|---|---|---|
Priority: | low | Milestone: | 8.4.1 |
Component: | Compiler | Version: | 8.2.1-rc2 |
Keywords: | backpack LevityPolymorphism | Cc: | Iceland_jack, tibbe, goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
In the code snippet below, I attempt to use backpack with levity polymorphism:
{-# LANGUAGE MagicHash #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} unit number-unknown where signature NumberUnknown where import GHC.Types data Number 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 type Number = Int plus :: Int -> Int -> Int plus = (+) multiply :: Int -> Int -> Int multiply = (*) unit number-unboxed-int where module NumberUnknown where import GHC.Prim 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 main = putStrLn "Hello world!"
Compiling this with ghc --backpack packer.bkp
fails with the following error:
- Type constructor ‘Number’ has conflicting definitions in the module and its hsig file Main module: type Number = GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep Hsig file: data Number The types have different kinds - while checking that number-unboxed-int:NumberUnknown implements signature NumberUnknown in number-unknown[NumberUnknown=number-unboxed-int:NumberUnknown] type Number = Int#
The error is pretty clear: Number
can only be instantiated by types of kind Type
(aka TYPE LiftedRep
). Even while remaining levity monomorphic, there doesn't seem to be a way to pick a different kind. For example, redefining Number
in the signature as
data Number :: TYPE IntRep
leads to the following immediate failure:
Kind signature on data type declaration has non-* return kind TYPE 'IntRep
I do not understand any of the internals of backpack, so I do not understand if there's anything fundamental that makes this impossible. Going one step further, I would like to be able to do something like this (the syntax here is not even currently valid for a backpack signature):
type MyRep :: RuntimeRep data Number :: TYPE MyRep
This may be instantiated with something like this:
type MyRep = IntRep type Number = Int#
And then end users would be able to monomorphize levity-polymorphic functions. This would be really neat because there is currently no way to do this in GHC.
So, I guess there are really two feature requests in here. One is the ability to use unlifted data types with backpack. The other is the ability to use backpack to monomorphize levity-polymorphic functions.
It seems unlikely to sneak this into GHC 8.2 but who knows!
Change History (7)
comment:1 Changed 15 months ago by
Cc: | Iceland_jack added |
---|
comment:2 Changed 15 months ago by
Cc: | tibbe added |
---|
comment:3 Changed 15 months ago by
comment:5 Changed 15 months ago by
Cc: | goldfire added |
---|---|
Description: | modified (diff) |
Here is a proof of concept patch which relaxes the "Kind signature on data type declaration has non-* return kind" check and fixes a bug (we're not currently renaming data type result kinds), which lets a modified version of the example work. Here's the patch:
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index 2e738c1ec6..b902b548a3 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -422,11 +422,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/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 9b313f0c60..1ba2388ed5 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1747,7 +1747,7 @@ tcDataKindSig :: Kind -> TcM ([TyConBinder], Kind) -- Returns the new TyVars, the extracted TyBinders, and the new, reduced -- result kind (which should always be Type or a synonym thereof) tcDataKindSig kind - = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind) + = do { return () -- checkTc (isLiftedTypeKind res_kind) (badKindSig kind) ; span <- getSrcSpanM ; us <- newUniqueSupply ; rdr_env <- getLocalRdrEnv diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index aadb7b5cad..0fd43eb228 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -691,18 +691,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_style = vcat [ pp_roles - , pp_nd <+> pp_lhs <+> pp_where + , pp_nd <+> pp_lhs <+> dcolon <+> ppr 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 <+> dcolon <+> ppr kind) 2 (add_bars pp_cons) , nest 2 $ ppShowIface ss pp_extra ] where is_data_instance = isIfaceDataInstance parent
And the working 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#))
To turn this into a real patch, we have to construct an appropriate conditional for when to apply the isLiftedTypeKind
test. Two main questions:
- Is this sound for hs-boot? I don't think so: how can we know how to generate code of an unknown representation? We need to know the correct size to allocate for it. (Actually, this is a pretty interesting case where double-vision cures would solve the problem.) This means this should only be permitted for abstract data types in hsig files, and we probably still need to assert that it's some sort of TYPE thing.
- Is
data F :: TYPE Rep
the syntax we want? It is a bit disingenous because, absented UnliftedDataTypes, the only way to actually implement one of these is with a type synonym. But it doesn't look that unnatural. We had a close miss when working on constraint synonyms (we ended up usingclass A
to declare an abstract constraint rather than allowingdata F :: Constraint
.
Pinging goldfire who may have opinions.
comment:7 Changed 11 months ago by
Milestone: | → 8.4.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
Yeah, this doesn't look something GHC allows right now, because
data
declarations have to have kind*
, and there is no way to define an abstract type with different kind. But it seems like it should be possible, we just have to relax some of the checks GHC does.