[Haskell-cafe] Parametric polymorphism and promoted types

[Artem Pelenitsyn]

Hey Marcin,

Discussed on the GHC bug tracker
https://gitlab.haskell.org/ghc/ghc/issues/17072

--
Best, Artem


On Wed, Oct 2, 2019, 6: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/20191002/ead048dc/attachment.html>