[GHC] #14198: Inconsistent treatment of implicitly bound kind variables as free-floating
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #7873 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- (Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.) This program is accepted: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo = MkFoo (forall a. Proxy a) }}} There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`: {{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}} This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But to make things stranger, it you write out the kind of `a` explicitly: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}} Then GHC will reject it: {{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} So GHC's treatment is inconsistent. What should GHC do? We could: * Have both be an error. * Have both be accepted, and implicitly quantify `k` as an existential type variable * Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is: {{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} * Something else. When you try a similar trick with type synonyms: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy type Foo3 = forall a. Proxy a }}} Instead of generalizing the kind of `a`, its kind will default to `Any`: {{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}} Would that be an appropriate trick for data types as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: Old description:
(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo = MkFoo (forall a. Proxy a) }}}
There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`:
{{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}}
This was brought up some time ago in #7873, where the conclusion was to keep this behavior.
But to make things stranger, it you write out the kind of `a` explicitly:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}}
Then GHC will reject it:
{{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}}
So GHC's treatment is inconsistent. What should GHC do? We could:
* Have both be an error. * Have both be accepted, and implicitly quantify `k` as an existential type variable * Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is:
{{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} * Something else. When you try a similar trick with type synonyms:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
type Foo3 = forall a. Proxy a }}}
Instead of generalizing the kind of `a`, its kind will default to `Any`:
{{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}}
Would that be an appropriate trick for data types as well?
New description: (Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.) This program is accepted: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo = MkFoo (forall a. Proxy a) }}} There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`: {{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}} This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable. But to make things stranger, it you write out the kind of `a` explicitly: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}} Then GHC will reject it: {{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} So GHC's treatment is inconsistent. What should GHC do? We could: * Have both be an error. * Have both be accepted, and implicitly quantify `k` as an existential type variable * Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is: {{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} * Something else. When you try a similar trick with type synonyms: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy type Foo3 = forall a. Proxy a }}} Instead of generalizing the kind of `a`, its kind will default to `Any`: {{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}} Would that be an appropriate trick for data types as well? -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Old description:
(Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.)
This program is accepted:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo = MkFoo (forall a. Proxy a) }}}
There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`:
{{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}}
This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable.
But to make things stranger, it you write out the kind of `a` explicitly:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}}
Then GHC will reject it:
{{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}}
So GHC's treatment is inconsistent. What should GHC do? We could:
* Have both be an error. * Have both be accepted, and implicitly quantify `k` as an existential type variable * Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is:
{{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} * Something else. When you try a similar trick with type synonyms:
{{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}
import Data.Proxy
type Foo3 = forall a. Proxy a }}}
Instead of generalizing the kind of `a`, its kind will default to `Any`:
{{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}}
Would that be an appropriate trick for data types as well?
New description: (Spun off from the discussion starting at https://phabricator.haskell.org/D3872#109927.) This program is accepted: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo = MkFoo (forall a. Proxy a) }}} There's something interesting going on here, however. Because `PolyKinds` is enabled, the kind of `a` is generalized to `k`. But where does `k` get quantified? It turns out that it's implicitly quantified as an existential type variable to `MkFoo`: {{{ λ> :i Foo data Foo = forall k. MkFoo (forall (a :: k). Proxy a) }}} This was brought up some time ago in #7873, where the conclusion was to keep this behavior. But it's strange becuase the `k` is existential, so the definition is probably unusable. But to make things stranger, it you write out the kind of `a` explicitly: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy data Foo2 = MkFoo2 (forall (a :: k). Proxy a) }}} Then GHC will reject it: {{{ Bug.hs:7:1: error: Kind variable ‘k’ is implicitly bound in data type ‘Foo2’, but does not appear as the kind of any of its type variables. Perhaps you meant to bind it (with TypeInType) explicitly somewhere? | 7 | data Foo2 = MkFoo2 (forall (a :: k). Proxy a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} So GHC's treatment is inconsistent. What should GHC do? We could: 1. Have both be an error. 2. Have both be accepted, and implicitly quantify `k` as an existential type variable 3. Have both be accepted, and implicitly quantify `k` in the `forall` itself. That is: {{{#!hs MkFoo :: (forall {k} (a :: k). Proxy k a) -> Foo }}} 4. Something else. When you try a similar trick with type synonyms: {{{#!hs {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} import Data.Proxy type Foo3 = forall a. Proxy a }}} Instead of generalizing the kind of `a`, its kind will default to `Any`: {{{ λ> :i Foo3 type Foo3 = forall (a :: GHC.Types.Any). Proxy a }}} Would that be an appropriate trick for data types as well? -- Comment (by goldfire): Nice description of the problem. I'll respond to your proposed solutions. 1. Yes. 2. No. H98 syntax should not be in the business of guessing existential variables. Existentials are a bit strange and should be strictly opt-in (at least for H98 syntax). 3. No. We stopped inferring kind quantification anywhere nested within a type with GHC 8. 4. We could do this, but I doubt it's what the user wants. Indeed, I think it would be an improvement to reject that type synonym, which is probably not what the user wants at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Going with option 1 (have both be an error) sounds fine to me. But I'm not quite sure what the error message should be when we encounter an inferred, free-floating kind variable, as in `data Foo = MkFoo (forall a. Proxy a)`, where the `k` in `(a :: k)` is inferred. We could go with the usual `Kind variable ‘k’ is implicitly bound in data type` fare, but users might find that befuddling. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think we actually have the opportunity for a good error message here. I ''think'' we'll know that the `k` is not user-written, because it will be `Inferred`, not `Specified`. So we can say that the variable was inferred instead of just calling it an inscrutable `k0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:4 goldfire]:
I ''think'' we'll know that the `k` is not user-written, because it will be `Inferred`, not `Specified`.
So you wish to perform free-floating checks on `TyConBinder`s instead of `TyVar`s? That might work... but wait. How would this work for data family instances? IIUC, they don't have anything like `TyConBinders`, so I'm not sure how we'd perform this check there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): OK. Perhaps I'm just wrong. I didn't look at the code to compose comment:4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14268 | Blocking: Related Tickets: #7873 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * blockedby: => 14268 Comment: Note that data family instances //will// gain `TyVarBndr`s once #14268 is implemented, so let's wait until that is done before coming back to this issue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14268 | Blocking: Related Tickets: #7873, #15474 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #7873 => #7873, #15474 Comment: See #15474 for another ticket about `type Foo3` in the original comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14268 | Blocking: Related Tickets: #7873, #15474 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14268 | Blocking: Related Tickets: #7873, #15474 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): https://gitlab.haskell.org/ghc/ghc/merge_requests/361 makes `reportFloatingKvs` obsolete, but we might want to restore it to fix this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14198: Inconsistent treatment of implicitly bound kind variables as free-floating -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: 14268 | Blocking: Related Tickets: #7873, #15474 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think this is subtly a different problem than `reportFloatingKvs`: that's all about user-written kind variables; this ticket is about overactive generalization. We ''could'' just say that `a` has kind `Any`. But I prefer rejecting the program. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14198#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC