[Haskell-cafe] Parametric polymorphism and promoted types

[Marcin Szamotulski]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 477 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191002/a0a057ce/attachment.sig>