[GHC] #14674: Deferring more levity polymorphism checks in indefinite backpack modules
GHC
ghc-devs at haskell.org
Fri Feb 2 01:03:28 UTC 2018
#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
More information about the ghc-tickets
mailing list