[Haskell-cafe] Parametric polymorphism and promoted types
Marcin Szamotulski
profunctor at pm.me
Wed Oct 2 22:19:11 UTC 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
-------------- 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>
More information about the Haskell-Cafe
mailing list