D2038: [WIP] TysPrim: Generalize kind of (->)

[Simon Peyton Jones]

Replying by email because I'm on  a train.

Simon

Huh.   Put otherwise, your point is this.  Suppose we
have the following kind for `(->)`:


   (->) :: forall v1 v2 r1 r2.  TYPE v1 r1 -> TYPE v2 r2 -> Type

To coerce from

   (C a -> Int) to (a -> Int)

we'd have to cough up a coercion `g`:


g :    (->) Vanilla    Vanilla Ptr Ptr (C a) Int

     ~R (->) Constraint Vanilla Ptr Ptr a     Int

And now (Nth 1 g :: Vanilla ~R Constraint).  Nothing about
`KindCo` there; it's just that `(->)` takes some kind
arguments.

But that can only happen if `(->)` has suitable roles.
What if it doesn't?

What if we just had an axiom


axArrow v ::    (->) Vanilla    v

             ~R (->) Constraint v

or something like that.   Then we get


[W] g :    (->) Vanilla    Vanilla Ptr Ptr (C a) Int

        ~R (->) Constraint Vanilla Ptr Ptr a     Int

We decompose partly and solve thus


g = (axArrow Vanilla) <Ptr> <Ptr> axC <Int>


Simon

From: noreply at phabricator.haskell.org [mailto:noreply at phabricator.haskell.org]
Sent: 31 January 2017 12:51
To: Simon Peyton Jones <simonpj at microsoft.com>
Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->)

goldfire added a comment.
View Revision<https://phabricator.haskell.org/D2038>


In D2038#89360<https://phabricator.haskell.org/D2038#89360>, @simonpj<https://phabricator.haskell.org/p/simonpj/> wrote:

To avoid being able to extract ContraintRep ~R LiftedPtrRep we decided to weaken one of the coercion constructors, the one that gets a kind coercion from a type coercion. We don't need it, and it's awkward here.

The problem is that we need it with this patch. I was able to weaken this coercion constructor (KindCo) in my patch D3023<https://phabricator.haskell.org/D3023>, but this patch uses it in a fundamental way that we can't get around. To wit:

class C a where

  meth :: a



axC :: (C a :: Constraint) ~R (a :: Type)

Now, we wish to cast C a -> a to a -> a.. This cast will look like (->) ?? <LiftedRep> axC <a>. What goes in the ??? It's got to be something involving KindCo axC, which is disallowed as per our earlier decision. Therein lies the problem.

As for reify: Yes, I'm agreed with that email. But is that implemented yet? Is a design settled on? I don't see a ghc-proposal. Are we wiling to take a dependency on that work in order to get this done?

To be clear, my chief worry isn't that these problems cannot be solved by any means -- I'm just worried about the timing of this all and our desire to get 8.2 out the door.

REPOSITORY
rGHC Glasgow Haskell Compiler

REVISION DETAIL
https://phabricator.haskell.org/D2038

EMAIL PREFERENCES
https://phabricator.haskell.org/settings/panel/emailpreferences/

To: bgamari, goldfire, austin
Cc: simonpj, RyanGlScott, thomie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170131/cd37bd43/attachment.html>