[GHC] #15928: Reduction stack overflow when using "coerce"

[GHC]

#15928: Reduction stack overflow when using "coerce"
-------------------------------------+-------------------------------------
        Reporter:  harendra          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  MacOS X           |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 If we ask GHC for the role signature on `Stream` (as you can with `:info`
 in GHCi), we learn that the `a` parameter has a phantom role. This means
 that `Stream Identity a` shares a representation with `Stream Identity a0`
 no matter what `a` and `a0` are. So GHC does not unify them. Instead, it
 simply doesn't care what `a0` is. It chooses `Any`. (We can see this with
 `-ddump-tc -fprint-typechecker-elaboration`).

 When you change the definition for `Stream`, `a` then gets a
 representational role, and so GHC is stuck trying to figure out what `a0`
 is, giving you the error you observe. If you say `type role Stream
 representational nominal`, then the program is accepted, because now GHC
 observes that `a0` must certainly be `a`. It does the unification and then
 succeeds.

 > If there is no bug then this needs to be explained in some simple way.

 I respectfully disagree with this statement. Though simplicity is always a
 goal, it cannot be achieved in all cases. In the end, the `coerce` feature
 was added to provide a performance boost when GHC can know that runtime
 representations of two types are the same. That knowledge -- i.e., knowing
 when two types are `Coercible` -- is subtle, which is why it took the
 research community three papers to figure it out. Even now, as you have
 observed, we have room to improve. (That is, the choice between `data` and
 `newtype` shouldn't matter here... but it does, because we don't know an
 algorithm that can work reliably with recursive newtypes.) One might argue
 that we should have never introduced `coerce` because the theory behind it
 is too complicated. For better or worse, the Haskell community tends to
 prefer complicated, powerful solutions over simple, less expressive ones.
 (Of course, we love simple, powerful ones!) And so we end up where we are
 today.

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