[Haskell-cafe] Parametric polymorphism and promoted types

[Richard Eisenberg]

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 <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/20191003/1304887b/attachment.html>