#15294 closed bug (wontfix)

Unused "foralls" prevent types from being Coercible

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.3
Keywords: Roles Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

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?

Change History (3)

comment:1 Changed 15 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 15 months ago by goldfire

I think this is expected behavior.

Representational equality still falls short of its goal of equating all things with equal representation. For example, Bool is not Coercible to data BBool = FFalse | TTrue, even though Bool and BBool (plausibly) have the same representation.

It's true that forall a. Int -> Bool and Int -> Bool have the same runtime representation, but they crucially look quite different in Core. A member of forall a. Int -> Bool looks like /\ (a :: Type). \ (x :: Int). ..., while a member of Int -> Bool looks like \ (x :: Int). .... One could imagine extending representational equality in this way (it would be sound, if we get the details right), but I don't think it's worth it.

comment:3 Changed 15 months ago by Iceland_jack

Resolution: wontfix
Status: newclosed

Ah yeah I see the difficulty, I wanted to make sure :) thanks for the response

closing

Note: See TracTickets for help on using tickets.