[GHC] #14674: Deferring more levity polymorphism checks in indefinite backpack modules

[GHC]

#14674: Deferring more levity polymorphism checks in indefinite backpack modules
-------------------------------------+-------------------------------------
        Reporter:  andrewthad        |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.4.1-alpha1
      Resolution:                    |             Keywords:  backpack
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by andrewthad):

 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14674#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler