Opened 15 months ago

Closed 15 months ago

## #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 )

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

Description: | modified (diff) |
---|

### comment:2 Changed 15 months ago by

### comment:3 Changed 15 months ago by

Resolution: | → wontfix |
---|---|

Status: | new → closed |

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

closing

**Note:**See TracTickets for help on using tickets.

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.