#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 ezyang)

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 13 months ago by Iceland_jack

Cc: Iceland_jack added

comment:2 Changed 13 months ago by tibbe

Cc: tibbe added

comment:3 Changed 13 months ago 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.

comment:4 Changed 13 months ago by Iceland_jack

UnliftedDataTypes is relevant

comment:5 Changed 13 months ago by ezyang

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:

  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.

comment:6 Changed 10 months ago by Ben Gamari <ben@…>

In fd8b044e/ghc:

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

comment:7 Changed 10 months ago by bgamari

Milestone: 8.4.1
Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.