[GHC] #14155: GHC mentions unlifted types out of the blue (to me anyway)

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | 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 one does me 'ead in, I accidentally type `Ran` instead of `Swap` {{{#!hs {-# Language RankNTypes, DerivingStrategies, TypeApplications, ScopedTypeVariables, GADTs, GeneralizedNewtypeDeriving, InstanceSigs, PolyKinds #-} import Data.Coerce newtype Ran g h a = Ran (forall b. (a -> g b) -> h b) newtype Swap p f g a where Swap :: p g f a -> Swap p f g a deriving newtype Show class IxPointed m where ireturn :: a -> m i i a instance IxPointed f => IxPointed (Swap f) where ireturn :: forall a i. a -> Swap f i i a ireturn a = Ran (ireturn a) }}} and get this error {{{ $ ghci -ignore-dot-ghci /tmp/bug.hs GHCi, version 8.3.20170605: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /tmp/bug.hs, interpreted ) /tmp/bug.hs:17:15: error: • Couldn't match expected type ‘Swap f i i a’ with actual type ‘Ran g0 h0 a0’ • In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) In the instance declaration for ‘IxPointed (Swap f)’ • Relevant bindings include a :: a (bound at /tmp/bug.hs:17:11) ireturn :: a -> Swap f i i a (bound at /tmp/bug.hs:17:3) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^^^^^^^ /tmp/bug.hs:17:20: error: • Couldn't match a lifted type with an unlifted type Expected type: (a0 -> g0 b) -> h0 b Actual type: (->) (a0 -> g0 b) (a0 -> g0 b) a • In the first argument of ‘Ran’, namely ‘(ireturn a)’ In the expression: Ran (ireturn a) In an equation for ‘ireturn’: ireturn a = Ran (ireturn a) | 17 | ireturn a = Ran (ireturn a) | ^^^^^^^^^ Failed, modules loaded: none. }}} Is GHC right to bring up unlifted types? I would guess this is due to the newly added levity polymorphism of `(->) :: TYPE rep -> TYPE rep' -> Type` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: 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 RyanGlScott): * cc: RyanGlScott (added) Comment: Here's a simpler version which removes some cruft: {{{#!hs newtype R a = R ((a -> a) -> a) newtype Swap p f g a = Swap (p g f a) class IxPointed m where ireturn :: a -> m i i a instance IxPointed f => IxPointed (Swap f) where ireturn a = R (ireturn a) }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:9:15: error: • Couldn't match expected type ‘Swap f i i a’ with actual type ‘R a’ • In the expression: R (ireturn a) In an equation for ‘ireturn’: ireturn a = R (ireturn a) In the instance declaration for ‘IxPointed (Swap f)’ • Relevant bindings include a :: a (bound at Bug.hs:9:11) ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3) | 9 | ireturn a = R (ireturn a) | ^^^^^^^^^^^^^ Bug.hs:9:18: error: • Couldn't match a lifted type with an unlifted type • In the first argument of ‘R’, namely ‘(ireturn a)’ In the expression: R (ireturn a) In an equation for ‘ireturn’: ireturn a = R (ireturn a) • Relevant bindings include a :: a (bound at Bug.hs:9:11) ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3) | 9 | ireturn a = R (ireturn a) | ^^^^^^^^^ }}} This is a regression form 8.0.2, where the error message didn't mention unlifted types: {{{ $ /opt/ghc/8.0.2/bin/ghci Bug.hs GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:9:15: error: • Couldn't match expected type ‘Swap f i i a’ with actual type ‘R a’ • In the expression: R (ireturn a) In an equation for ‘ireturn’: ireturn a = R (ireturn a) In the instance declaration for ‘IxPointed (Swap f)’ • Relevant bindings include a :: a (bound at Bug.hs:9:11) ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3) Bug.hs:9:18: error: • Couldn't match type ‘m0 (a -> a)’ with ‘(->)’ Expected type: (a -> a) -> a Actual type: m0 (a -> a) (a -> a) a • In the first argument of ‘R’, namely ‘(ireturn a)’ In the expression: R (ireturn a) In an equation for ‘ireturn’: ireturn a = R (ireturn a) • Relevant bindings include a :: a (bound at Bug.hs:9:11) ireturn :: a -> Swap f i i a (bound at Bug.hs:9:3) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: 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 Iceland_jack): This feels similar {{{#!hs -- /tmp/bug.hs:6:12-20: error: -- • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ -- When matching the kind of ‘'GHC.Types.LiftedRep’ -- • In the first argument of ‘R’, namely ‘(m `ibind`)’ -- In the expression: R (m `ibind`) -- In an equation for ‘lft’: lft m = R (m `ibind`) -- | -- 6 | lft m = R (m `ibind`) -- | ^^^^^^^^^ -- Failed, modules loaded: none. newtype R a = R ((a -> a) -> a) class IxMonad m where ibind :: (a -> m j k b) -> m i j a -> m i k b lft m = R (m `ibind`) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 simonpj): * keywords: => TypeInType * priority: normal => highest * milestone: => 8.4.1 Comment: Aha. Based on comment:1 I very rapidly found that the constraint solver was going wrong thus. We have {{{ m :: k0 -> k0 -> * -> * i :: k0 }}} and a wanted constraint {{{ [W] (m i :: k0 -> * -> *) ~# ((->) LR LR :: * -> * -> *) }}} where `LR` is `LiftedRep`. This much is fine. But then the canonicaliser decomposes it thus {{{ [W] (i :: k0) ~# (LR :: *) [W] (m :: k0 -> k0 -> * -> *) ~# ((->) LR :: forall r. * -> TYPE r -> *) }}} which is utterly bogus. Presumably we need an extra guard in the `can_eq_app` that checks that neither function kind is a forall? Richard please comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 goldfire): Agreed with extra check -- but it should check for the fact that neither is a forall or both are foralls. I don't see a problem in decomposing a dependent application in this way. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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): OK: might you do this? Not hard, it seems. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 goldfire): Sure. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 bgamari): * priority: highest => high Comment: This doesn't seem like a truly "highest" priority issue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 bgamari): * milestone: 8.4.1 => 8.6.1 Comment: What is the status of this, goldfire? Regardless, it's unlikely that this will happen for 8.4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 bgamari): * owner: (none) => goldfire -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.4.2 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 bgamari): * priority: high => normal * milestone: 8.6.1 => 8.4.2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14155: GHC mentions unlifted types out of the blue (to me anyway) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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 bgamari): * milestone: 8.4.2 => 8.6.1 Comment: Bumping off to 8.6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14155#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC