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

[Richard Eisenberg]

> On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
>  
> But that can only happen if `(->)` has suitable roles.
> What if it doesn’t?

The “correct” roles for (->) of the kind you gave is `nominal nominal nominal nominal representational representational`. That is, the dependent arguments are nominal, and the others are representational. This is because all kind-level coercions are nominal. You seem to be suggesting giving (->) different roles. I honestly don’t know what that would mean -- normally, GHC prevents you from specifying a weaker role than it would infer. It smells pretty foul to me, but I can’t quite put my finger on what would go wrong at the moment.

>  
> What if we just had an axiom
>  
> axArrow v ::    (->) Vanilla    v
>              ~R (->) Constraint v

I think we’d also need one for results... but maybe not.

>  
> 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>

And this works only if we weaken (->)’s roles.

This whole road just feels like the wrong way, as soon as we started contemplating a heterogeneous axiom, which are ruled out in the literature, even when we have kind equalities.

I think the Right Answer is to get rid of newtype-classes & fix reify, and I’m worried that anything short of that will fail catastrophically at some point. Otherwise, it’s patches on top of patches.

I don’t think there is disagreement here, but there is the question about what to do for 8.2.... and unless we’re ready to roll out the new reify, I think the best course of action is to delay the new Typeable and all this Constraint v Type stuff until 8.4. (The new levity polymorphism stuff already committed is hunky-dory.)

Richard

>  
>  
> Simon
>   <>
> From: noreply at phabricator.haskell.org <mailto:noreply at phabricator.haskell.org> [mailto: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 <mailto: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 patchD3023 <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 <https://phabricator.haskell.org/D2038>
>  
> EMAIL PREFERENCES
> https://phabricator.haskell.org/settings/panel/emailpreferences/ <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/3818cc6f/attachment-0001.html>