[GHC] #11715: Constraint vs *

[GHC]

#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