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