Deferring more levity polymorphism checks in indefinite backpack modules

This is kind of a follow up issue to issue #13955 (closed). I'm able to get along a little further with the thing I'm trying to do. Here's a minimal example. The number-example-a and number-example-b sections are not really needed to trigger the problem. They are included as examples of how the signature might be instantiated.

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

unit the-fam where
  module TheFamily where
    import Data.Kind
    import GHC.Types
    import GHC.Prim
    data Liftedness = Lifted | Unlifted
    data SingLiftedness (x :: Liftedness) where
      SingLifted :: SingLiftedness 'Lifted
      SingUnlifted :: SingLiftedness 'Unlifted
    type family LiftednessIntRep (x :: Liftedness) :: RuntimeRep where
      LiftednessIntRep 'Lifted = LiftedRep
      LiftednessIntRep 'Unlifted = IntRep
    type family LiftednessInt (x :: Liftedness) :: TYPE (LiftednessIntRep x) where
      LiftednessInt 'Lifted = Int
      LiftednessInt 'Unlifted = Int#

unit number-indefinite where
  dependency the-fam
  signature NumberUnknown where
    import GHC.Types
    import TheFamily
    data MyLiftedness :: Liftedness
  module NumberStuff where
    import NumberUnknown
    import TheFamily
    identityInt :: LiftednessInt MyLiftedness -> LiftednessInt MyLiftedness
    identityInt i = i

unit number-example-a where
  dependency the-fam
  module NumberUnknown where
    import GHC.Types
    import TheFamily
    type MyLiftedness = Lifted
    identityInt :: Int -> Int
    identityInt x = x

unit number-example-b where
  dependency the-fam
  module NumberUnknown where
    import GHC.Types
    import GHC.Prim
    import TheFamily
    type MyLiftedness = Unlifted
    identityInt :: Int# -> Int#
    identityInt i = i

unit main where
  dependency number-indefinite[NumberUnknown=number-example-a:NumberUnknown]
  module Main where
    import NumberStuff
    import GHC.Types
    main = print (identityInt 5)

Attempting to compile with the ghc 8.4 release candidate gives:

> /usr/local/bin/ghc-8.4.0.20171214 --backpack small_levity_backpack.bkp
small_levity_backpack.bkp:35:17: error:
    A levity-polymorphic type is not allowed here:
      Type: LiftednessInt MyLiftedness
      Kind: TYPE (LiftednessIntRep MyLiftedness)
    In the type of binder ‘i’
   |
35 |     identityInt i = i
   |                 ^

I disagree with this error. The type of i is not actually levity polymorphic in either of the example instantiations of the signature. If this check were omitted from the type-checking of the indefinite module, I suspect that this code should be able to compile and run fine.

I'm not sure if there's a good general rule for when to suppress these checks in indefinite modules and when to not suppress them. Clearly, there are some cases were a function will with a levity-polymorphic binder no matter how the signature is fulfilled, and those ideally should continue to be rejected. And there are other cases like the one I raise here where it's guaranteed to be safe. There are other cases where the whether or not there's a levity-polymorphic binder depends on the instantiation:

data X = X1 | X2
type family Rep (a :: X) (r :: RuntimeRep) :: RuntimeRep
  Rep X1 r = r
  Rep X2 r = UnliftedRep

And then finally, there are situations where it's always going to lead to a levity-polymorphic binder, but it isn't feasible for the compiler to figure that out. A sufficiently tricky type family would cause this.

Sorry this was a bit of a ramble. I think there actually is a good rule for this. Defer the levity-polymorphic binder check in indefinite modules any time the type-checker encounters a type variable whose RuntimeRep is a type family that cannot be reduced. The check will happen later any way, and more correct code will be accepted.

Trac metadata

Trac field	Value
Version	8.4.1-alpha1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ezyang, goldfire
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import backpack labels

Another more simple solution to this problem would be to add a flag that could only be used with indefinite modules named -fdefer-levity-check. This would entirely disable the binder rule for indefinite modules where it was turned on.

With this patch, I can get my example code to compile:

diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 3f893dbcb2..3a50fd2d3c 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -2348,7 +2348,7 @@ isTypeLevPoly = go
     go ty@(TyVarTy {})                           = check_kind ty
     go ty@(AppTy {})                             = check_kind ty
     go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
-                          | otherwise            = check_kind ty
+                          | otherwise            = False -- check_kind ty
     go (ForAllTy _ ty)                           = go ty
     go (FunTy {})                                = False
     go (LitTy {})                                = False

Of course, this is not acceptable since it disables the levity binder check for type families in both indefinite modules and in conventional modules. Just for context, here is the full function definition (before applying the above patch):

-- | Returns True if a type is levity polymorphic. Should be the same
-- as (isKindLevPoly . typeKind) but much faster.
-- Precondition: The type has kind (TYPE blah)
isTypeLevPoly :: Type -> Bool
isTypeLevPoly = go
  where
    go ty@(TyVarTy {})                           = check_kind ty
    go ty@(AppTy {})                             = check_kind ty
    go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False
                          | otherwise            = False -- check_kind ty
    go (ForAllTy _ ty)                           = go ty
    go (FunTy {})                                = False
    go (LitTy {})                                = False
    go ty@(CastTy {})                            = check_kind ty
    go ty@(CoercionTy {})                        = pprPanic "isTypeLevPoly co" (ppr ty)

    check_kind = isKindLevPoly . typeKind

One way to solve this is to make isTypeLevPoly take an additional argument that tells it what type of module we are in. But there might be an easier solution. I don't what TyCon indefinite data types (is that what they are called?) like MyLiftedness are represented in GHC. I'm guessing that it's AlgTyCon. There may be something inside AlgTyCon that can be used to figure out where of not it's an indefinite data type (for example, if it has a kind other than Type and it isn't a builtin type). If that's the case, then in the TyConApp check above, we could check to see if we're looking at a type family. If so, if any on the arguments are indefinite data types, then we could say that it's alright, since this could only happen in an indefinite module. I need feedback on this since though I'm not familiar with these things.

We need Edward!

I just realized a huge problem with what I'm trying to do. It doesn't even work when there isn't any levity polymorphism involved. Behold:

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

unit the-fam where
  module TheFamily where
    import Data.Kind
    data Universe = Red | Green
    data SingUniverse (x :: Universe) where
      SingRed :: SingUniverse 'Red
      SingGreen :: SingUniverse 'Green
    type family Interpret (x :: Universe) :: Type where
      Interpret 'Red = Bool
      Interpret 'Green = Int

unit number-indefinite where
  dependency the-fam
  signature NumberUnknown where
    import GHC.Types
    import TheFamily
    data MyUniverse :: Universe
  module NumberStuff where
    import NumberUnknown
    import TheFamily
    universalDefault :: SingUniverse MyUniverse -> Interpret MyUniverse
    universalDefault SingRed = True
    universalDefault SingGreen = 55

unit main where
  module Main where
    main :: IO ()
    main = print (identityInt 5)

This is rejected with:

backpack_type_refinement.bkp:30:32: error:
    • Could not deduce: Interpret MyUniverse ~ Bool
      from the context: MyUniverse ~ 'Red
        bound by a pattern with constructor: SingRed :: SingUniverse 'Red,
                 in an equation for ‘universalDefault’
        at backpack_type_refinement.bkp:30:22-28
    • In the expression: True
      In an equation for ‘universalDefault’:
          universalDefault SingRed = True
   |
30 |     universalDefault SingRed = True
   |                                ^^^^

And with a similar error for the subsequent line. It is entirely reasonable for this to be rejected. I'm going to close this ticket for now and reconsider my approach to what I'm trying to accomplish.

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Pnormal label