#14185: Non-local bug reporting around levity polymorphism -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | LevityPolymorphism, | TypeErrorMessages 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): I looked at this in an odd moment. This instance {{{ instance (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where unbox (a,b) = (# unbox a, unbox b #) box (# a, b #) = (box a, box b) }}} is quantified over four type variables, ''all of which get kind `Type`''. But in `testTup` we will need to solve {{{ [W] Unbox (Int, Char) (# Int#, Char# ) }}} That is well-kinded but it doesn't match the instance (which has only lifted type variables). What ''actually'' happens is that we try to solve {{{ [W] Unbox (Int,Char) alpha }}} and the fundep says `alpha := (# beta, gamma #)`, but since the fundep comes from the tuple instance, it insists that `beta::*` and `gamma::*`. If you try to make the instance levity-polymorphic: {{{ instance forall a b ar br (a' :: TYPE r1) (b' :: TYPE br). (Unbox a a', Unbox b b') => Unbox (a,b) (# a', b' #) where }}} it rightly fails with {{{ T14185a.hs:23:10: error: A levity-polymorphic type is not allowed here: Type: a' Kind: TYPE r1 In the type of binder ‘a’ | 23 | box (# a, b #) = (box a, box b) | ^ }}} This does not explain why we get bogus errors in `testInt` but I claim there is no bug in rejecting `testTup`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14185#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler