<div dir="auto">Hey Marcin,<div dir="auto"><br></div><div dir="auto">Discussed on the GHC bug tracker</div><div dir="auto"><a href="https://gitlab.haskell.org/ghc/ghc/issues/17072">https://gitlab.haskell.org/ghc/ghc/issues/17072</a><br></div><div dir="auto"><br></div><div dir="auto">--</div><div dir="auto">Best, Artem</div><br><br><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Wed, Oct 2, 2019, 6:19 PM Marcin Szamotulski via Haskell-Cafe <<a href="mailto:haskell-cafe@haskell.org">haskell-cafe@haskell.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Haskell Cafe,<br>
<br>
It seems that GHC has a trouble recognising that a variable of type <br>
<br>
`forall (x :: (a, b))` can be reduced to `forall ((u, v) :: (a, b))`. <br>
<br>
For example in the following snippet `unsafeCoerce` is unavoidable:<br>
<br>
```<br>
data P a = P<br>
<br>
data Proxy (p :: (a, b)) where<br>
    Proxy :: P a -> P b -> Proxy '(a, b)<br>
<br>
both0 :: forall (s :: (a, b)).  Proxy s<br>
both0 = unsafeCoerce (Proxy P P)<br>
```<br>
<br>
<br>
A slightly nicer solution can be written with type families:<br>
<br>
```<br>
type family Fst (p :: (a, b)) :: a where<br>
  Fst '(x, y) = x<br>
<br>
type family Snd (p :: (a, b)) :: b where<br>
  Snd '(x, y) = y<br>
<br>
data Dict (a :: k) (b :: k) where<br>
    Dict :: a ~ b => Dict a b<br>
<br>
instance Category Dict where<br>
    id = Dict<br>
    Dict . Dict = Dict<br>
<br>
proof :: forall (s :: (a, b)). Dict s '(Fst s, Snd s)<br>
proof = unsafeCoerce Dict<br>
<br>
both1 :: forall (s :: (a, b)).  Proxy s<br>
both1 = case proof :: Dict s '(Fst s, Snd s) of<br>
    Dict -> Proxy P P<br>
```<br>
<br>
Did I missed how to avoid `unsafeCoerce` all together?<br>
<br>
Best regards,<br>
Marcin Szamotulski_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div></div>