[GHC] #11518: Test TcCoercibleFail hangs with substitution sanity checks enabled

[GHC]

#11518: Test TcCoercibleFail hangs with substitution sanity checks enabled
-------------------------------------+-------------------------------------
        Reporter:  niteria           |                Owner:  niteria
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  performance bug                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by niteria):

 No, I don't think the example from comment:14 is related.

 We have
 {{{
 newtype VoidBad a = VoidBad (VoidBad (a,a))
 foo5' = coerce :: (VoidBad ()) -> ()
 }}}

 For `coerce :: (VoidBad ()) -> ()` to typecheck we have to know if
 `VoidBad ()` and `()` have the same runtime representation.
 So we need to find out what `VoidBad ()` really is. So we start unwrapping
 the newtypes of off it.

 What do we get when we try to unwrap the newtype off of `VoidBad ()`?

 {{{
 VoidBad () = VoidBad ((),())
 = VoidBad (((),()),((),()))
 = VoidBad ((((),()),((),())),(((),()),((),())))
 = ...
 }}}

 It's clear that the type we apply to `VoidBad` grows exponentially and
 that `VoidBad ()` diverges. Before adding the ASSERT this is detected by
 `checkRecTc`. The reason that `checkRecTc` manages to do that in the
 presence of an exponentially growing argument to `VoidBad` is that
 `checkRecTc` only counts how many times we've applied `VoidBad`. It never
 looks at the exponentially growing argument.

 The reason why we are able to build an exponentially growing arguments
 with small amount of space and time has to do with sharing. When we apply
 `VoidBad a = VoidBad (a, a)` it is the *same* `a` that goes to the left
 and right component of the pair. The `a` is shared between both
 components.

 The way we apply `VoidBad a = VoidBad (a, a)` is by using the `substTy`
 function. We replace every `a` from the right hand side with `a` from the
 left hand side. But in this case we use the *same* `a`, so the size of the
 type grows exponentially, but the representation doesn't.

 The problem arises when `substTy` examines the argument we passed as `a`
 to look for the free vars to do the ASSERT. Since the type grows
 exponentially, the time to compute the free vars also grows exponentially
 and we don't get to the 100th iteration of unwrapping in any reasonable
 amount of time.

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