[GHC] #16334: Named wildcards in kinds
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.4 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This works: {{{ Prelude> :set -XNamedWildCards -XPartialTypeSignatures -XPolyKinds Prelude> k :: (Int :: _); k = 42 <interactive>:2:14: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘*’ • In the type signature: k :: (Int :: _) }}} And this doesn't: {{{ Prelude> k :: (Int :: _t); k = 42 <interactive>:3:7: error: • Expected kind ‘_t’, but ‘Int’ has kind ‘*’ • In the type signature: k :: (Int :: _t) }}} The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason. I plan to fix it as part of https://gitlab.haskell.org/ghc/ghc/merge_requests/361 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.4.4 checker) | Keywords: Resolution: | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => PartialTypeSignatures -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.4.4 checker) | Keywords: Resolution: | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/361 -------------------------------------+------------------------------------- Changes (by int-index): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/361 Old description:
This works:
{{{ Prelude> :set -XNamedWildCards -XPartialTypeSignatures -XPolyKinds Prelude> k :: (Int :: _); k = 42
<interactive>:2:14: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘*’ • In the type signature: k :: (Int :: _) }}}
And this doesn't:
{{{ Prelude> k :: (Int :: _t); k = 42
<interactive>:3:7: error: • Expected kind ‘_t’, but ‘Int’ has kind ‘*’ • In the type signature: k :: (Int :: _t) }}}
The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason. I plan to fix it as part of https://gitlab.haskell.org/ghc/ghc/merge_requests/361
New description: This works: {{{ Prelude> :set -XNamedWildCards -XPartialTypeSignatures -XPolyKinds Prelude> k :: (Int :: _); k = 42 <interactive>:2:14: warning: [-Wpartial-type-signatures] • Found type wildcard ‘_’ standing for ‘*’ • In the type signature: k :: (Int :: _) }}} And this doesn't: {{{ Prelude> k :: (Int :: _t); k = 42 <interactive>:3:7: error: • Expected kind ‘_t’, but ‘Int’ has kind ‘*’ • In the type signature: k :: (Int :: _t) }}} The issue, I suspect, is in `partition_nwcs`, which ignores kind variables for some reason. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.4.4 checker) | Keywords: Resolution: fixed | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T16334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/361 -------------------------------------+------------------------------------- Changes (by int-index): * status: patch => closed * testcase: => T16334 * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.4.4 checker) | Keywords: Resolution: fixed | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T16334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/361 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.10.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16334: Named wildcards in kinds -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.4.4 checker) | Keywords: Resolution: fixed | PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: T16334 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/361 -------------------------------------+------------------------------------- Comment (by Marge Bot <ben+marge-bot@…>): In [changeset:"5bc195b1fe788e9a900a15fbe473967850517c3e/ghc" 5bc195b1/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5bc195b1fe788e9a900a15fbe473967850517c3e" Treat kind/type variables identically, demolish FKTV Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024 -no-kind-vars.rst Fixes Trac #16334, Trac #16315 With this patch, scoping rules for type and kind variables have been unified: kind variables no longer receieve special treatment. This simplifies both the language and the implementation. User-facing changes ------------------- * Kind variables are no longer implicitly quantified when an explicit forall is used: p :: Proxy (a :: k) -- still accepted p :: forall k a. Proxy (a :: k) -- still accepted p :: forall a. Proxy (a :: k) -- no longer accepted In other words, now we adhere to the "forall-or-nothing" rule more strictly. Related function: RnTypes.rnImplicitBndrs * The -Wimplicit-kind-vars warning has been deprecated. * Kind variables are no longer implicitly quantified in constructor declarations: data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) -- no longer accepted data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b) -- still accepted Related function: RnTypes.extractRdrKindSigVars * Implicitly quantified kind variables are no longer put in front of other variables: f :: Proxy (a :: k) -> Proxy (b :: j) f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b -- old order f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -- new order This is a breaking change for users of TypeApplications. Note that we still respect the dpendency order: 'k' before 'a', 'j' before 'b'. See "Ordering of specified variables" in the User's Guide. Related function: RnTypes.rnImplicitBndrs * In type synonyms and type family equations, free variables on the RHS are no longer implicitly quantified unless used in an outermost kind annotation: type T = Just (Nothing :: Maybe a) -- no longer accepted type T = Just Nothing :: Maybe (Maybe a) -- still accepted The latter form is a workaround due to temporary lack of an explicit quantification method. Ideally, we would write something along these lines: type T @a = Just (Nothing :: Maybe a) Related function: RnTypes.extractHsTyRdrTyVarsKindVars * Named wildcards in kinds are fixed (Trac #16334): x :: (Int :: _t) -- this compiles, infers (_t ~ Type) Related function: RnTypes.partition_nwcs Implementation notes -------------------- * One of the key changes is the removal of FKTV in RnTypes: - data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName] - , fktv_tys :: [Located RdrName] } + type FreeKiTyVars = [Located RdrName] We used to keep track of type and kind variables separately, but now that they are on equal footing when it comes to scoping, we can put them in the same list. * extract_lty and family are no longer parametrized by TypeOrKind, as we now do not distinguish kind variables from type variables. * PatSynExPE and the related Note [Pattern synonym existentials do not scope] have been removed (Trac #16315). With no implicit kind quantification, we can no longer trigger the error. * reportFloatingKvs and the related Note [Free-floating kind vars] have been removed. With no implicit kind quantification, we can no longer trigger the error. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16334#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC