Hi Marcin, This is a long-standing feature request in GHC (see https://gitlab.haskell.org/ghc/ghc/issues/7259). System FC doesn't have eta-laws for products, i.e. it does not have forall (s :: (a, b)) . s ~ '(Fst s, Snd s) even though in principle it should be sound to add such axioms to the theory. Unfortunately in practice adding such axioms would currently be unsound due to #14420. As you've observed, one can essentially assert such an axiom using unsafeCoerce. There are various different ways to package this up nicely, but they all involve equivalent forms of unsafety, and all are type-unsound in the presence of #14420. Although the unsoundness is unlikely to bite unless you really try... I've attached a module illustrating this. Hope this helps, Adam On 02/10/2019 23:19, 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
-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England