[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
#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
: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