[GHC] #16013: :kind! accepts unsaturated type aliases
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 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: -------------------------------------+------------------------------------- Here's a ghci session: {{{
:set -XTypeFamilies -XPolyKinds type family Id (a :: k) type instance Id a = a type Foo x = Maybe :kind! Id Foo Id Foo :: * = Id Foo }}}
I think the final `:kind!` query should throw an error instead, complaining that `Foo` hasn't been given enough arguments. (But even if you disagree, and think it should be allowed, `*` is clearly not the right kind!) Using a normal type alias in place of the type family for `Id` also allows the query incorrectly, though it does at least report a sensible kind. Although I think it shouldn't matter, I have checked with `-ignore-dot- ghci` to make sure I haven't accidentally turned LiberalTypeSynonyms on. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 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 dmwit): Okay, so further thinking, I'd like to retract part of the complaint. I believe I understand why it decides on kind `*`, and agree that's a sensible answer. (Namely: I thought in my head `Id :: k -> k`, but the compiler chose `Id :: k -> *`, following exactly the rules set out in the documentation, so the compiler was right and I was wrong. And I thought in my head `Id a = a` matches all types so `Id Foo` should reduce to `Foo` if it works at all, but the compiler thought `Id a = a` only matches when `a :: *`, so `Id Foo` is a stuck term not one that can reduce, and again the compiler was right and I was wrong.) But I still think it should probably complain about applying a type family or type alias to an unsaturated type alias. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13962 Comment: `:kind` deliberately allows unsaturated uses of type synonyms and type families—see [https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/ghci.html #ghci-cmd-:kind this section] of the users' guide. Many folks find it quite handy to be able to query the kinds of type synonyms with `:kind` (e.g., `:kind Id`), but disallowing unsaturated type synonyms/families //carte blanche// would prevent `:kind Id` from working, so a special case was added to allow it in that particular scenario. (Also note that this has been previously discussed in #13962.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dmwit): Sure, I understand the motivation. It seems like a sensible middle ground would be to special-case only top- level unsaturated type aliases/families, and not wholesale allow unsaturation. And indeed the way the documentation was written makes it sound like that's the case: it uses the precise language ":kind even allows you to write a partial application of a type synonym", whereas `Id Foo` is not a partial application of a type synonym but rather the application of a type (family) to a partial application of a type synonym. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:3 dmwit]:
whereas `Id Foo` is not a partial application of a type synonym but rather the application of a type (family) to a partial application of a type synonym.
Indeed. Still, removing this feature would be a breaking change (albeit a slight one), so that's something to consider. It might be worth opening a [https://github.com/ghc-proposals/ghc-proposals GHC proposal] about this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): My own vote is that we drop the saturation requirement only at top-level, calling the current implementation a bug. To my horror, GHC allows this interaction: {{{#!hs type family Map f x where Map _ '[] = '[] Map f (x : xs) = f x : Map f xs data Nat = Zero | Succ Nat type family Pred n where Pred Zero = Zero Pred (Succ n) = n }}} {{{ λ> :kind! Map Pred [Succ (Succ Zero), Succ (Succ (Succ Zero)), Zero] Map Pred [Succ (Succ Zero), Succ (Succ (Succ Zero)), Zero] :: [Nat] = '[ 'Succ 'Zero, 'Succ ('Succ 'Zero), 'Zero] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
My own vote is that we drop the saturation requirement only at top- level, calling the current implementation a bug.
I'm fine with this. Ryan, might you execute on this? Thanks! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Are we OK with pushing through a breaking change without an accompanying GHC proposal? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I'm OK with that. This is a bug, and this ticket proposes a fix. I don't think a proposal is needed. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Phab:D5471 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5471 Comment: Alright, then here's a patch. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Phab:D5471, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/90 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * differential: Phab:D5471 => Phab:D5471, https://gitlab.haskell.org/ghc/ghc/merge_requests/90 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/should_fail/T16013 Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Phab:D5471, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/90 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => ghci/should_fail/T16013 * resolution: => fixed * milestone: => 8.8.1 Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/6b70cf611e5ddc475edaa54b893d209906... 6b70cf611e5ddc475edaa54b893d20990699ddb8]: {{{ commit 6b70cf611e5ddc475edaa54b893d20990699ddb8 Author: Ryan Scott <ryan.gl.scott@gmail.com> Date: Tue Jan 8 07:37:18 2019 -0500 Be pickier about unsaturated synonyms in :kind Summary: We currently permit any and all uses of unsaturated type synonyms and type families in GHCi's `:kind` command, which allows strange interactions like this one: ``` > :set -XTypeFamilies -XPolyKinds > type family Id (a :: k) > type instance Id a = a > type Foo x = Maybe > :kind! Id Foo ``` This is probably a stretch too far, so this patch moves to disallow unsaturated synonyms that aren't at the top level (we still want to allow `:kind Id`, for instance). We do this by augmenting `GhciCtxt` with an additional `Bool` field to indicate if we are at the outermost level of the type being passed to `:kind` or not. See `Note [Unsaturated type synonyms in GHCi]` in `TcValidity` for the full story. Test Plan: make test TEST=T16013 Reviewers: goldfire, bgamari Reviewed By: goldfire Subscribers: simonpj, goldfire, rwbarton, carter GHC Trac Issues: #16013 Differential Revision: https://phabricator.haskell.org/D5471 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16013: :kind! accepts unsaturated type aliases -------------------------------------+------------------------------------- Reporter: dmwit | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | ghci/should_fail/T16013 Blocked By: | Blocking: Related Tickets: #13962 | Differential Rev(s): Phab:D5471, Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/90 -------------------------------------+------------------------------------- Comment (by Ryan Scott <ryan.gl.scott@…>): In [changeset:"6b70cf611e5ddc475edaa54b893d20990699ddb8/ghc" 6b70cf6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6b70cf611e5ddc475edaa54b893d20990699ddb8" Be pickier about unsaturated synonyms in :kind Summary: We currently permit any and all uses of unsaturated type synonyms and type families in GHCi's `:kind` command, which allows strange interactions like this one: ```
:set -XTypeFamilies -XPolyKinds type family Id (a :: k) type instance Id a = a type Foo x = Maybe :kind! Id Foo
This is probably a stretch too far, so this patch moves to disallow
unsaturated synonyms that aren't at the top level (we still want to
allow `:kind Id`, for instance). We do this by augmenting `GhciCtxt`
with an additional `Bool` field to indicate if we are at the
outermost level of the type being passed to `:kind` or not. See
`Note [Unsaturated type synonyms in GHCi]` in `TcValidity` for the
full story.
Test Plan: make test TEST=T16013
Reviewers: goldfire, bgamari
Reviewed By: goldfire
Subscribers: simonpj, goldfire, rwbarton, carter
GHC Trac Issues: #16013
Differential Revision: https://phabricator.haskell.org/D5471
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16013#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
participants (1)
-
GHC