[GHC] #15979: Core Lint error with LiberalTypeSynonyms
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE LiberalTypeSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# OPTIONS_GHC -dcore-lint #-} module Bug where import Data.Kind type KindOf (a :: k) = k wat :: KindOf (forall (a :: ()). a) wat = () }}} {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: In the type ‘KindOf (forall (a :: ()). a)’ Non-*-like kind when *-like expected: () when checking the body of forall: forall (a :: ()). a *** Offending Program *** Rec { $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Bug"#) wat :: KindOf (forall (a :: ()). a) [LclIdX] wat = () end Rec } *** End of Offense *** <no location info>: error: Compilation had errors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Is it just me, or does this Core Lint check seem entirely bogus? This seems to assume that the body of a `forall` will always be `*`-kinded, but that's just blatantly false (`forall (f :: Type -> Type). f` is another counterexample.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): No, the Lint check is right. The kinding rules for types are given in comment:4 of #15791. And, I assume, in `docs/core-spec`. So the bug is in the type checker which should reject the program. It's not easy to do that for type inference, because we lack a constraint that says "This kind should be either (TYPE r) or Constraint". I think the easiest way to fix this would be in `checkValidType`; and specifically in the code you have just been working on in `check_type`. In a sigma-type (the code you moved up) add a test that the kind of the body is `TYPE r` or `Constraint`. Richard, right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Uh... what? I must be living in a different reality, then, since GHC has always let me do this without complaint: {{{#!hs type Foo = forall (f :: Type -> Type). f }}} So either I'm taking crazy pills, or those kinding rules for types are blatantly wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: goldfire (added) Comment: Let's ask Richard, but I think it should never have accepted that -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another one: {{{#!hs {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} module Bug where import Data.Kind type Foo = forall (f :: Type -> Type). f f :: Foo Int -> Foo Int f x = x }}} {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: In the type ‘Foo Int -> Foo Int’ Non-*-like kind when *-like expected: * -> * when checking the body of forall: forall (f :: * -> *). f *** Offending Program *** Rec { $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Bug"#) f :: Foo Int -> Foo Int [LclIdX] f = \ (x_aWa :: Foo Int) -> x_aWa end Rec } *** End of Offense *** <no location info>: error: Compilation had errors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): This //passes// `-dcore-lint`, however: {{{#!hs {-# LANGUAGE RankNTypes #-} module Works where f :: (forall. Maybe) a f = Nothing }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): `forall (f :: Type -> Type). f` is bogus. It should be rejected both by the type checker and Core Lint. This is rather awkward w.r.t. type inference (as Simon points out) because of `Constraint`. I don't like the validity-checking solution, because then we reject something like `:k forall a. a` in GHCi. `a`'s kind will be unconstrained, so it will get kind `k`. But then the `forall` is bogus. We could imagine a magic class `TypeLike` with `instance TypeLike (TYPE r)` and `instance TypeLike Constraint`. We can further imagine defaulting this class (not unlike how we default `Num`). But this is a sledgehammer of a solution, to be sure. I don't think there is anything unsound about removing the restriction... but no published type theory (to my knowledge) does so. Back in the day, the restriction wasn't there because we needed, e.g., `forall a. Array# a` -- that is, we needed unlifted types (which didn't really have kinds) in `forall`s. Now with levity polymorphism, we have a more principled way of dealing with this all, and so we do. Perhaps the new principles weren't carried all the way to their logical conclusion, though, as this ticket shows. Note: if we really can't come up with a good way to impose this restriction in the type-checker, I wouldn't be strongly opposed to just dropping it. It's just a little smelly, but no worse than that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Interestingly, there appears to be some sort of check for this already, but only when kind-checking. Given this: {{{#!hs data P k :: k -> Type }}} Then GHC accept the following: {{{#!hs type Foo = forall k (a :: k). P k a }}} However, it does //not// accept the following: {{{#!hs type Bar = forall k. P k }}} {{{ $ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:10:22: error: • Expected kind ‘k0’, but ‘P k’ has kind ‘k -> *’ • In the type ‘forall k. P k’ In the type declaration for ‘Bar’ | 10 | type Bar = forall k. P k | ^^^ }}} The current error message doesn't really give a clear indication as to the underlying cause, however. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15979: Core Lint error with LiberalTypeSynonyms -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I think comment:8 is quite a separate matter: see the kinding rule for foralls in #15791 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15979#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC