[Haskell-cafe] Parametric polymorphism and promoted types
Marcin Szamotulski
profunctor at pm.me
Fri Oct 4 20:04:11 UTC 2019
Thanks Artem, Adam and Richard for the code, explanation and links, it's makes the problem clear.
Best regards,
Marcin
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Thursday, 3 October 2019 08:14, Richard Eisenberg <rae at richarde.dev> wrote:
> This *is* on the GHC issue tracker, but I think the ticket Artem has linked to is about a different concern. I think you want #7259 (https://gitlab.haskell.org/ghc/ghc/issues/7259). Right now, doing this expansion is potentially unsound, actually, as the type system can be abused to make a (p :: (a, b)) that is not a pair. :(
>
> Further research needs to be done before we know how to fix this, sadly.
>
> Richard
>
> > On Oct 2, 2019, at 11:19 PM, Marcin Szamotulski via Haskell-Cafe <haskell-cafe at haskell.org> wrote:
> >
> > Hello Haskell Cafe,
> >
> > It seems that GHC has a trouble recognising that a variable of type
> >
> > `forall (x :: (a, b))` can be reduced to `forall ((u, v) :: (a, b))`.
> >
> > For example in the following snippet `unsafeCoerce` is unavoidable:
> >
> > ```
> > data P a = P
> >
> > data Proxy (p :: (a, b)) where
> > Proxy :: P a -> P b -> Proxy '(a, b)
> >
> > both0 :: forall (s :: (a, b)). Proxy s
> > both0 = unsafeCoerce (Proxy P P)
> > ```
> >
> > A slightly nicer solution can be written with type families:
> >
> > ```
> > type family Fst (p :: (a, b)) :: a where
> > Fst '(x, y) = x
> >
> > type family Snd (p :: (a, b)) :: b where
> > Snd '(x, y) = y
> >
> > data Dict (a :: k) (b :: k) where
> > Dict :: a ~ b => Dict a b
> >
> > instance Category Dict where
> > id = Dict
> > Dict . Dict = Dict
> >
> > proof :: forall (s :: (a, b)). Dict s '(Fst s, Snd s)
> > proof = unsafeCoerce Dict
> >
> > both1 :: forall (s :: (a, b)). Proxy s
> > both1 = case proof :: Dict s '(Fst s, Snd s) of
> > Dict -> Proxy P P
> > ```
> >
> > Did I missed how to avoid `unsafeCoerce` all together?
> >
> > Best regards,
> > Marcin Szamotulski_______________________________________________
> > Haskell-Cafe mailing list
> > To (un)subscribe, modify options or view archives go to:
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> > Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191004/e175095a/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 477 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191004/e175095a/attachment.sig>
More information about the Haskell-Cafe
mailing list