[Haskell-cafe] Parametric polymorphism and promoted types

[Adam Gundry]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: EtaProducts.hs
Type: text/x-haskell
Size: 1047 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20191003/8618a17f/attachment.hs>