<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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 (<a href="https://gitlab.haskell.org/ghc/ghc/issues/7259" class="">https://gitlab.haskell.org/ghc/ghc/issues/7259</a>). 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. :(<div class=""><br class=""></div><div class="">Further research needs to be done before we know how to fix this, sadly.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Oct 2, 2019, at 11:19 PM, Marcin Szamotulski via Haskell-Cafe <<a href="mailto:haskell-cafe@haskell.org" class="">haskell-cafe@haskell.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">Hello Haskell Cafe,<br class=""><br class="">It seems that GHC has a trouble recognising that a variable of type <br class=""><br class="">`forall (x :: (a, b))` can be reduced to `forall ((u, v) :: (a, b))`. <br class=""><br class="">For example in the following snippet `unsafeCoerce` is unavoidable:<br class=""><br class="">```<br class="">data P a = P<br class=""><br class="">data Proxy (p :: (a, b)) where<br class=""> Proxy :: P a -> P b -> Proxy '(a, b)<br class=""><br class="">both0 :: forall (s :: (a, b)). Proxy s<br class="">both0 = unsafeCoerce (Proxy P P)<br class="">```<br class=""><br class=""><br class="">A slightly nicer solution can be written with type families:<br class=""><br class="">```<br class="">type family Fst (p :: (a, b)) :: a where<br class=""> Fst '(x, y) = x<br class=""><br class="">type family Snd (p :: (a, b)) :: b where<br class=""> Snd '(x, y) = y<br class=""><br class="">data Dict (a :: k) (b :: k) where<br class=""> Dict :: a ~ b => Dict a b<br class=""><br class="">instance Category Dict where<br class=""> id = Dict<br class=""> Dict . Dict = Dict<br class=""><br class="">proof :: forall (s :: (a, b)). Dict s '(Fst s, Snd s)<br class="">proof = unsafeCoerce Dict<br class=""><br class="">both1 :: forall (s :: (a, b)). Proxy s<br class="">both1 = case proof :: Dict s '(Fst s, Snd s) of<br class=""> Dict -> Proxy P P<br class="">```<br class=""><br class="">Did I missed how to avoid `unsafeCoerce` all together?<br class=""><br class="">Best regards,<br class="">Marcin Szamotulski_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br class=""></div></div></body></html>