Changes between Initial Version and Version 5 of Ticket #13955


Ignore:
Timestamp:
Jul 12, 2017 3:10:25 AM (16 months ago)
Author:
ezyang
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.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #13955

    • Property Cc Iceland_jack tibbe goldfire added
  • Ticket #13955 – Description

    initial v5  
    8484
    8585So, 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.
     86
     87It seems unlikely to sneak this into GHC 8.2 but who knows!