[GHC] #14674: Deferring more levity polymorphism checks in indefinite backpack modules
#14674: Deferring more levity polymorphism checks in indefinite backpack modules -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Keywords: backpack | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is kind of a follow up issue to issue #13955. 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14674 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14674#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 simonpj): We need Edward! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14674#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#14674: Deferring more levity polymorphism checks in indefinite backpack modules -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: invalid | 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: | -------------------------------------+------------------------------------- Changes (by andrewthad): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14674#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC