[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):

 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.

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