[GHC] #10075: Muddling Constraint and * means that Core is inconsistent

[GHC]

#10075: Muddling Constraint and * means that Core is inconsistent
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.8.4
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 I can say this:

 {{{
 type family F (a :: k)

 type instance F (a :: Constraint) = Int
 type instance F (a :: *)          = Bool
 }}}

 This compiles to the following Core:

 {{{
 F :: forall (k :: BOX). k -> *
 axF1 :: [a :: Constraint].F Constraint a ~ Int
 axF2 :: [a :: *].         F *          a ~ Bool
 }}}

 I can then build the following:

 {{{
 sym axF1[Any Constraint] ; axF2[Any *] :: Int ~ Bool
 }}}

 The transitivity is sound because, in Core, `Constraint` and `*` are
 indistinguishable.

 I don't think there's a way to actually cause a bug in a running program
 due to this problem, but we should probably patch it up.

 Possible resolution: Have `coreView` change `Constraint` to `*`.

 Possible resolution once we have `* :: *`: Make `Constraint` and `*`
 representationally equal. In other words, it would be as if `Constraint`
 were a newtype around `*`. I haven't thought out the ramifications of this
 decision, but there's something nice about it.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10075>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler