[Haskell-cafe] Parametric polymorphism and promoted types

[Marcin Szamotulski]

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>