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: [email protected] [mailto:[email protected]]
Sent: 31 January 2017 12:51
To: Simon Peyton Jones <[email protected]>
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
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
