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.