[GHC] #13955: Backpack does not handle unlifted types
GHC
ghc-devs at haskell.org
Wed Jul 12 03:10:25 UTC 2017
#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 at 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 at 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
More information about the ghc-tickets
mailing list