<div>Thanks Artem, Adam and Richard for the code, explanation and links, it's makes the problem clear.<br><br>Best regards,<br>Marcin<br></div><div class="protonmail_signature_block protonmail_signature_block-empty"><div class="protonmail_signature_block-user protonmail_signature_block-empty"><br></div><div class="protonmail_signature_block-proton protonmail_signature_block-empty"><br></div></div><div><br></div><div>‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐<br></div><div> On Thursday, 3 October 2019 08:14, Richard Eisenberg <rae@richarde.dev> wrote:<br></div><div> <br></div><blockquote class="protonmail_quote" type="cite"><div>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. :(<br></div><div class><br></div><div class>Further research needs to be done before we know how to fix this, sadly.<br></div><div class><br></div><div class><div>Richard<br></div><div class><div><div><br></div><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:<br></div><div><br></div><div class><div class><div>Hello Haskell Cafe,<br></div><div><br></div><div>It seems that GHC has a trouble recognising that a variable of type <br></div><div><br></div><div>`forall (x :: (a, b))` can be reduced to `forall ((u, v) :: (a, b))`. <br></div><div><br></div><div>For example in the following snippet `unsafeCoerce` is unavoidable:<br></div><div><br></div><div>```<br></div><div>data P a = P<br></div><div><br></div><div>data Proxy (p :: (a, b)) where<br></div><div>    Proxy :: P a -> P b -> Proxy '(a, b)<br></div><div><br></div><div>both0 :: forall (s :: (a, b)).  Proxy s<br></div><div>both0 = unsafeCoerce (Proxy P P)<br></div><div>```<br></div><div><br></div><div><br></div><div>A slightly nicer solution can be written with type families:<br></div><div><br></div><div>```<br></div><div>type family Fst (p :: (a, b)) :: a where<br></div><div>  Fst '(x, y) = x<br></div><div><br></div><div>type family Snd (p :: (a, b)) :: b where<br></div><div>  Snd '(x, y) = y<br></div><div><br></div><div>data Dict (a :: k) (b :: k) where<br></div><div>    Dict :: a ~ b => Dict a b<br></div><div><br></div><div>instance Category Dict where<br></div><div>    id = Dict<br></div><div>    Dict . Dict = Dict<br></div><div><br></div><div>proof :: forall (s :: (a, b)). Dict s '(Fst s, Snd s)<br></div><div>proof = unsafeCoerce Dict<br></div><div><br></div><div>both1 :: forall (s :: (a, b)).  Proxy s<br></div><div>both1 = case proof :: Dict s '(Fst s, Snd s) of<br></div><div>    Dict -> Proxy P P<br></div><div>```<br></div><div><br></div><div>Did I missed how to avoid `unsafeCoerce` all together?<br></div><div><br></div><div>Best regards,<br></div><div>Marcin Szamotulski_______________________________________________<br></div><div>Haskell-Cafe mailing list<br></div><div>To (un)subscribe, modify options or view archives go to:<br></div><div><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></div><div>Only members subscribed via the mailman list are allowed to post.<br></div></div></div></blockquote></div></div></div></blockquote><div><br></div>