Opened 4 years ago

Closed 3 years ago

Last modified 2 years ago

#11714 closed feature request (fixed)

Kind of (->) type constructor is overly constrained

Reported by: bgamari Owned by: bgamari
Priority: highest Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: Typeable, LevityPolymorphism Cc:
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 (last modified by bgamari)

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,

(->) :: 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.

Change History (15)

comment:1 Changed 4 years ago by bgamari

As described in ticket:11011#comment:40, the current constrained kind of (->) causes Core lint violations on my wip/ttypeable branch. The Core lint violation in T11120 mentioned in that comment 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,

mkTrApp @* @* @((->) Char#) @CharHash ...

which was produced as evidence for the Typeable representation for,

data CharHash = CharHash Char#
Last edited 3 years ago by bgamari (previous) (diff)

comment:2 Changed 4 years ago by goldfire

(->) :: 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.

comment:3 Changed 4 years ago 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?

comment:4 Changed 4 years ago by goldfire

Maybe. We'd have to write it and test its performance.

comment:5 Changed 3 years ago by bgamari

For what it's worth I took a stab at carrying out comment:3 here (also posted at Phab:D2038). At the moment I'm a bit stuck on how to deal with Constraints. This appears to be yet another case where * ~ Constraint would simplify things

Last edited 3 years ago by bgamari (previous) (diff)

comment:6 Changed 3 years ago by simonpj

Keywords: Typeable added

comment:7 Changed 3 years ago by bgamari

Description: modified (diff)

comment:8 Changed 3 years ago by bgamari

Keywords: LevityPolymorphism added

comment:9 Changed 3 years ago 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?

comment:10 Changed 3 years ago by bgamari

Owner: set to goldfire

Simon has said that Richard will be picking this up.

comment:11 Changed 3 years ago by bgamari

Priority: normalhigh

Bumping priority of this since the Typeable rework is contingent on it.

comment:12 Changed 3 years ago by bgamari

Owner: changed from goldfire to bgamari
Priority: highhighest

comment:13 Changed 3 years ago by Ben Gamari <ben@…>

In b207b53/ghc:

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.

comment:14 Changed 3 years ago by bgamari

Resolution: fixed
Status: newclosed

comment:15 Changed 2 years ago by Ryan Scott <ryan.gl.scott@…>

In ab27fdcf/ghc:

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
Note: See TracTickets for help on using tickets.