I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it. On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind. So, I propose: 1. Hold off on Constraint v Type until after the branch is cut. 2. Do what we can to mitigate Constraint v Type confusion vis-a-vis Typeable. (For example, make sure that there aren't Typeable instances for both, and have TcTypeable provide the Type instance whenever the Constraint instance is requested.) 3. Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous. 4. On the Constraint v Type patch, restore the full power of KindCo. This makes the type system broken, but I don't think the sky will come crashing down. 5. Merge Constraint v Type after the branch is cut. This will make GHC HEAD unsound in a new way, but no one will notice unless they try. 6. File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world). 7. Finish the first-class reification design and implement before 8.4. 8. Remove newtype-classes, thus eliminating heterogeneous axioms and the unsoundness mentioned in (5). This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.) What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type. Richard

On Jan 31, 2017, at 5:56 PM, Richard Eisenberg wrote:

...

On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones mailto:simonpj@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@phabricator.haskell.org mailto:noreply@phabricator.haskell.org [mailto:noreply@phabricator.haskell.org mailto:noreply@phabricator.haskell.org] Sent: 31 January 2017 12:51 To: Simon Peyton Jones mailto:simonpj@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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org mailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

1. Hold off on Constraint v Type until after the branch is cut. Good idea. I think that’d be OK. It’s no worse than the status quo. I’m MUCH more keen to get the TypeRep stuff in, because it has been in the works for nearly two years!! So let’s do 1-3 pronto. Who is acting there. Just Ben? Or are there bits Richard needs to help with? As to 4 onwards I still want to talk to you about roles. Simon From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] Sent: 01 February 2017 01:19 To: Simon Peyton Jones Cc: ghc-devs@haskell.org Subject: Re: D2038: [WIP] TysPrim: Generalize kind of (->) I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it. On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind. So, I propose: 1. Hold off on Constraint v Type until after the branch is cut. 2. Do what we can to mitigate Constraint v Type confusion vis-a-vis Typeable. (For example, make sure that there aren't Typeable instances for both, and have TcTypeable provide the Type instance whenever the Constraint instance is requested.) 3. Advertise that GHC will be a little confused on this point, and that, as far as Typeable is concerned, Constraint and Type are synonymous. 4. On the Constraint v Type patch, restore the full power of KindCo. This makes the type system broken, but I don't think the sky will come crashing down. 5. Merge Constraint v Type after the branch is cut. This will make GHC HEAD unsound in a new way, but no one will notice unless they try. 6. File a priority-highest bug to eliminate newtype-classes (which beget heterogeneous axioms in the Constraint/=Type world). 7. Finish the first-class reification design and implement before 8.4. 8. Remove newtype-classes, thus eliminating heterogeneous axioms and the unsoundness mentioned in (5). This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.) What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type. Richard On Jan 31, 2017, at 5:56 PM, Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote: On Jan 31, 2017, at 5:41 PM, Simon Peyton Jones mailto:simonpj@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@phabricator.haskell.orgmailto:noreply@phabricator.haskell.org [mailto:noreply@phabricator.haskell.org] Sent: 31 January 2017 12:51 To: Simon Peyton Jones mailto:simonpj@microsoft.com> Subject: [Differential] [Commented On] D2038: [WIP] TysPrim: Generalize kind of (->) goldfire added a comment. View Revisionhttps://phabricator.haskell.org/D2038 In D2038#89360https://phabricator.haskell.org/D2038#89360, @simonpjhttps://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 patchD3023https://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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Check out https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.2.1 There are several tickets you own in highest or high prio. Notably #12919 (an outright bug). And #12670, #13160, #13202 BEN: yell for whatever help you need with (->) and Typable Simon From: Richard Eisenberg [mailto:rae@cs.brynmawr.edu] Sent: 01 February 2017 13:54 To: Simon Peyton Jones Cc: ghc-devs@haskell.org Subject: Re: D2038: [WIP] TysPrim: Generalize kind of (->) On Feb 1, 2017, at 3:34 AM, Simon Peyton Jones mailto:simonpj@microsoft.com> wrote: Who is acting there. Just Ben? Or are there bits Richard needs to help with? Ben has done the real heavy lifting, with me opining on this bit or that. From what Ben says, it's very close. There is a small bit of new work to be done to prefer Type over Constraint when solving for Typeable (my step 2), but that can't be hard. If I'm released (for now) from #11715, what's the next priority for me? Richard