[GHC] #11714: Kind of (->) type constructor is overly constrained
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
#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`, 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
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
#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`, 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
#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
participants (1)
-
GHC