[GHC] #11714: Kind of (->) type constructor is overly constrained
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature | Status: new request | Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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: -------------------------------------+------------------------------------- Currently the `(->)` type constructor has kind `* -> * -> *` (with some magic to make infix work for unlifted types. To quote the comment attached to `TysPrim.funTyCon`,
You might think that `(->)` should have type `?? -> ? -> *`, and you'd be right. But if we do that we get kind errors when saying {{{ instance Control.Arrow (->) }}} because the expected kind is `* -> * -> *`. The trouble is that the expected/actual stuff in the unifier does not go contra-variant, whereas the kind sub-typing does. Sigh. It really only matters if you use `(->)` in a prefix way, thus: `(->) Int# Int#`. And this is unusual. because they are never in scope in the source }}}
This seems to imply that the restrictive kind arose out of the old subkinding story. Now that we have a more principled way of dealing with non-lifted kinds it seems we allow prefix uses to be as polymorphic as infix uses. Something like, {{{#!hs (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep). TYPE rep1 -> TYPE rep2 -> * }}} Not only would this be a win for consistency, but it may also address some of the Core Lint issues that I'm seeing in #11011. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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 bgamari): As described in ticket:11011#comment:39, the current constrained kind of `(->)` causes Core lint violations on my `wip/ttypeable` branch. The Core lint violation in `T11120` mentioned appears to be the result of `(->)` overly constrained kind when used in prefix position, `* -> * -> *`, {{{ Kind application error in type ‘(->) Char#’ Function kind = * -> * -> * Arg kinds = [(Char#, TYPE 'WordRep)] }}} Where this type appears in a use of `mkTrApp`, {{{#!hs mkTrApp @* @* @((->) Char#) @CharHash ... }}} which was produced as evidence for the `Typeable` representation for, {{{#!hs data CharHash = CharHash Char# }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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 goldfire):
{{{#!hs (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep). TYPE rep1 -> TYPE rep2 -> * }}}
Yes, this is exactly what we need. But I daresay this will be a performance disaster, littering Core with extra `RuntimeRep` arguments at every arrow, and requiring a substitution to get `->`'s kind. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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 simonpj): Maybe we can have * Saturated applications of arrow, with its own kinding rule. Actually it's represented as `ForAllTy (Anon ty1) ty2` so looks nothing like `TyConApp`, and there is no `TyCon` involved. * `(->)` with the complicated kind you give above, used for unsaturated partial applications. Now `splitTyConApp` on a `ForallTy (Anon _) _` would have to add those missing kind `RuntimeRep` arguments, but it can do that easily enough. Might that get the best of both worlds? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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 goldfire): Maybe. We'd have to write it and test its performance. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 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 bgamari): For what it's worth I took a stab at carrying out comment:3 [[http://git.haskell.org/ghc.git/commitdiff/refs/heads/wip/generalized- arrow|here]]. At the moment I'm a bit stuck on how to deal with `Constraint`s. This appears to be yet another case where `* ~ Constraint` would simplify things. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Typeable -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: @@ -13,3 +13,2 @@ - in a prefix way, thus: `(->) Int# Int#`. And this is unusual. - because they are never in scope in the source - }}} + in a prefix way, thus: `(->) Int# Int#`. And this is unusual because + they are never in scope in the source New description: Currently the `(->)` type constructor has kind `* -> * -> *` (with some magic to make infix work for unlifted types. To quote the comment attached to `TysPrim.funTyCon`,
You might think that `(->)` should have type `?? -> ? -> *`, and you'd be right. But if we do that we get kind errors when saying {{{ instance Control.Arrow (->) }}} because the expected kind is `* -> * -> *`. The trouble is that the expected/actual stuff in the unifier does not go contra-variant, whereas the kind sub-typing does. Sigh. It really only matters if you use `(->)` in a prefix way, thus: `(->) Int# Int#`. And this is unusual because they are never in scope in the source
This seems to imply that the restrictive kind arose out of the old subkinding story. Now that we have a more principled way of dealing with non-lifted kinds it seems we allow prefix uses to be as polymorphic as infix uses. Something like, {{{#!hs (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep). TYPE rep1 -> TYPE rep2 -> * }}} Not only would this be a win for consistency, but it may also address some of the Core Lint issues that I'm seeing in #11011. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * keywords: Typeable => Typeable, LevityPolymorphism -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism 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 simonpj): I think that in the paper, and verbally, we've converged on simply generalising the kind of `(->)`, as described in the Description. Shall we just do that? Richard? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: => goldfire Comment: Simon has said that Richard will be picking this up. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: feature request | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * priority: normal => high Comment: Bumping priority of this since the Typeable rework is contingent on it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: feature request | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: goldfire => bgamari * priority: high => highest -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: feature request | Status: new Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Typeable, | LevityPolymorphism 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 Ben Gamari <ben@…>): In [changeset:"b207b536ded40156f9adb168565ca78e1eef2c74/ghc" b207b53/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b207b536ded40156f9adb168565ca78e1eef2c74" Generalize kind of the (->) tycon This is generalizes the kind of `(->)`, as discussed in #11714. This involves a few things, * Generalizing the kind of `funTyCon`, adding two new `RuntimeRep` binders, ```lang=haskell (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). a -> b -> * ``` * Unsaturated applications of `(->)` are expressed as explicit `TyConApp`s * Saturated applications of `(->)` are expressed as `FunTy` as they are currently * Saturated applications of `(->)` are expressed by a new `FunCo` constructor in coercions * `splitTyConApp` needs to ensure that `FunTy`s are split to a `TyConApp` of `(->)` with the appropriate `RuntimeRep` arguments * Teach CoreLint to check that all saturated applications of `(->)` are represented with `FunTy` At the moment I assume that `Constraint ~ *`, which is an annoying source of complexity. This will be simplified once D3023 is resolved. Also, this introduces two known regressions, `tcfail181`, `T10403` ===================== Only shows the instance, instance Monad ((->) r) -- Defined in ‘GHC.Base’ in its error message when -fprint-potential-instances is used. This is because its instance head now mentions 'LiftedRep which is not in scope. I'm not entirely sure of the right way to fix this so I'm just accepting the new output for now. T5963 (Typeable) ================ T5963 is now broken since Data.Typeable.Internals.mkFunTy computes its fingerprint without the RuntimeRep variables that (->) expects. This will be fixed with the merge of D2010. Haddock performance =================== The `haddock.base` and `haddock.Cabal` tests regress in allocations by about 20%. This certainly hurts, but it's also not entirely unexpected: the size of every function type grows with this patch and Haddock has a lot of functions in its heap. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: feature request | Status: closed Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: Typeable, | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11714: Kind of (->) type constructor is overly constrained -------------------------------------+------------------------------------- Reporter: bgamari | Owner: bgamari Type: feature request | Status: closed Priority: highest | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: Typeable, | LevityPolymorphism 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 Ryan Scott <ryan.gl.scott@…>): In [changeset:"ab27fdcfe26759f3e4cd7e2105e7e7e83e269e48/ghc" ab27fdcf/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="ab27fdcfe26759f3e4cd7e2105e7e7e83e269e48" Add regression test for #13603 Summary: Commit b207b536ded40156f9adb168565ca78e1eef2c74 (#11714) happened to fix #13603 as well. Let's add a regression test so that it stays fixed. Test Plan: make test TEST=T13603 Reviewers: bgamari, austin, simonpj Reviewed By: bgamari, simonpj Subscribers: simonpj, rwbarton, thomie GHC Trac Issues: #13603 Differential Revision: https://phabricator.haskell.org/D3489 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11714#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC