Skip to content

Unused "foralls" prevent types from being Coercible

Just a quick question, do these have the same representation?

newtype A where
  A :: (Int -> Bool) -> A

newtype B where
  B :: (forall (a::Type). Int -> Bool) -> B

I'm wondering because they aren't Coercible

> :t coerce :: A -> B

<interactive>:1:1: error:
    • Couldn't match representation of type ‘forall a. Int -> Bool’
                               with that of ‘Int -> Bool’
        arising from a use of ‘coerce’
    • In the expression: coerce :: A -> B

C isn't Coercible to B either

newtype C where
  C :: (forall k (a :: k). Int -> Bool) -> C

Also

-- D is not Coercible to E, "can't match type ‘Bool’ with ‘Ordering’"

newtype D where
  D :: (forall (a::Bool) (b::Ordering). Int -> Bool) -> D

newtype E where
  E :: (forall (a::Ordering) (b::Bool). Int -> Bool) -> E

My question is is this intended?

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information