[GHC] #16255: Visible kind application defeats type family with higher-rank result kind
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.7 (Type checker) | Keywords: | Operating System: Unknown/Multiple TypeApplications, TypeFamilies | Architecture: | Type of failure: GHC accepts Unknown/Multiple | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: #15740 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- After #15740, GHC now (correctly) rejects this program: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind data SBool :: Bool -> Type type family F :: forall k. k -> Type where F = SBool }}} {{{ $ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.7.20190115: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:12:7: error: • Expected kind ‘forall k. k -> *’, but ‘SBool’ has kind ‘Bool -> *’ • In the type ‘SBool’ In the type family declaration for ‘F’ | 12 | F = SBool | ^^^^^ }}} However, there's a very simple way to circumvent this: add a visible kind application to `F`'s equation. {{{#!hs type family F :: forall k. k -> Type where F @Bool = SBool }}} If I understand things correctly, GHC shouldn't allow this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You understand things correctly. The arity checker probably only looks at the visible arity, which is correct, and the kind, which is also correct. Of course, that's clearly not the whole story. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Your hunch is correct, since [https://gitlab.haskell.org/ghc/ghc/blob/7cdcd3e12a5c3a337e36fa80c64bd72e5ef7... the current implementation] of the arity checker ignores invisible arguments entirely: {{{#!hs -- this check reports an arity error instead of a kind error; easier for user ; let vis_pats = numVisibleArgs hs_pats ; checkTc (vis_pats == vis_arity) $ wrongNumberOfParmsErr vis_arity ... where vis_arity = length (tyConVisibleTyVars tc_fam_tc) }}} I wonder if fixing this check is as simple as adding another `checkTc` for the number of specified arguments? Something like: {{{#!hs ; let invis_pats = length hs_pats - vis_pats ; checkTc (invis_pats <= specified_arity) $ error "You done goofed" ... where specified_arity = length [ tv | Bndr tv vis <- tyConBinders tc , tyConBndrVisArgFlag vis == Specified ] }}} I can only think of one place where this sort of thing could go wrong. If you instantiate a specified argument with `forall a. a`, then you could theoretically do something like this: {{{#!hs type family F :: k where -- One specified binder... F @(forall a. a) @Bool = True -- ...but two specified arguments! }}} That being said, GHC currently doesn't allow type family definitions like this one: {{{ • Illegal polymorphic type: forall a. a • In the equations for closed type family ‘F’ In the type family declaration for ‘F’ }}} So perhaps this isn't an issue in practice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I have no idea what that `F` would mean if it were allowed. Thankfully, it's not. I don't think it's as simple as that arity check, though. Witness {{{#!hs type family F (x :: j) :: forall k. Either j k where F 5 @Symbol = Left 4 }}} That looks well-kinded to me, it has the right visible arity, and it has the right specified arity, but it's still wrong. To get this right, I think we have to look not at the overall specified arity, but the specified arity ''after the last visible argument''. If we get that right, I think we've gotten this aspect right. (Note that a problem before the last visible argument must necessarily be a kind error, not an arity error.) That's a bit gross, but I think it will work. This should probably be done in the validity checker. The spot you've edited above is in the kind-checker. The only reason the visible arity check is done there is because it gives a nicer error message. These checks morally ought to be later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:3 goldfire]:
This should probably be done in the validity checker.
How would that possibly work? By the time we're in the validity checker, all we have are `CoAxBranch`es, which don't distinguish between required and specified arguments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ah, I just realized the answer to my own question: this information is (indirectly) stored in the `tyConBinders` of the type family tycon. We'd have to do a little bit of reverse engineering to recover which type patterns had which visibility, but it should be possible (I think). Another challenge is figuring out a good `SrcSpan` to use in the error message, which we don't have any location info in `TcValidity`. Maybe we'll just have to settle for the `SrcSpan` of the entire type family equation? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/260 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/260 * milestone: => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16255: Visible kind application defeats type family with higher-rank result kind -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Keywords: Resolution: | TypeApplications, TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC accepts | Test Case: invalid program | typecheck/should_fail/T16255 Blocked By: | Blocking: Related Tickets: #15740 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/260 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => typecheck/should_fail/T16255 * status: patch => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16255#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC