[Haskell-cafe] Parametric polymorphism and promoted types

2 Oct 2019

      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