#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Typeable, Resolution: | LevityPolymorphism, Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): There is a counterargument to the need to find a ''sound'' solution. Assume `type family F`. In GHC 8.0, you can say {{{ type instance F Constraint = Int type instance F Type = Bool }}} In GHC 8.4, you will also be able to say this, as `Constraint` will be fully distinct from `Type`. But comment:69 and comment:70 propose to disallow these instances in 8.2. This is certainly quite strange from a user standpoint! Instead, perhaps we live with the unsoundness, as long as the user can't find out. My guess is that the user's only way of finding out is via `Typeable`, which would need to reinforced against such attacks. (Specifically, arrange to make sure that the rep for `Constraint` is distinct from that for `Type`.) But I think we can do this. I very much don't like the idea of unsoundness in Core, but it won't be the only way to implement `unsafeCoerce`, and continuing to allow those instances provides a smoother experience to the user. Credit to @yav, who provoked me into actually suggesting to live with unsoundness! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:73 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler