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@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.

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 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.