[GHC] #13955: Backpack does not handle unlifted types

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature | Status: new request | Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Keywords: backpack | Operating System: Unknown/Multiple LevityPolymorphism | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by tibbe): * cc: tibbe (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): UnliftedDataTypes is relevant -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: low | Milestone: Component: Compiler | Version: 8.2.1-rc2 Resolution: | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ezyang): * cc: goldfire (added) @@ -101,0 +101,2 @@ + + It seems unlikely to sneak this into GHC 8.2 but who knows! New description: 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! -- Comment: 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: 1. 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. 2. 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 using `class A` to declare an abstract constraint rather than allowing `data F :: Constraint`. Pinging goldfire who may have opinions. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13955: Backpack does not handle unlifted types
-------------------------------------+-------------------------------------
Reporter: andrewthad | Owner: (none)
Type: feature request | Status: new
Priority: low | Milestone:
Component: Compiler | Version: 8.2.1-rc2
Resolution: | Keywords: backpack
| LevityPolymorphism
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari

#13955: Backpack does not handle unlifted types -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: closed Priority: low | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1-rc2 Resolution: fixed | Keywords: backpack | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13955#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC