[GHC] #15552: Infinite loop/panic with an existential type.

[GHC]

#15552: Infinite loop/panic with an existential type.
-------------------------------------+-------------------------------------
        Reporter:  howtonotwin       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:  TypeInType,
                                     |  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14723            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 (written concurrently with commen:8)

 After some discussion, Simon and I agreed that (1) from comment:7 would
 nab this bug. But many other questions/observations came up:

 A. This bug is caused by an optimization. What if we don't do the
 optimization? How much is performance affected? We hypothesize: not much.
 This is because while the optimization increases sharing in both time and
 space, this sharing is soon lost (in space, at least) in further passes.

 B. Interestingly, the other zonker (`zonkTcType` and friends in !TcMType)
 does not do this optimization. It could, and it wouldn't be plagued by
 this bug, as `TyCon`s aren't zonked there. So we've done the optimization
 in precisely the places we shouldn't.

 C. The optimization doesn't quite go far enough. Consider `alpha := beta
 -> beta` and `beta := Maybe (Int, Bool)`. Zonking `alpha` replaces the
 contents of the cell with `Maybe (Int, Bool) -> Maybe (Int, Bool)` instead
 of `beta -> beta`. But the next time we zonk `alpha`, we'll still walk
 over the large type `Maybe (Int, Bool) -> Maybe (Int, Bool)`.

 Simon and I puzzled on (C) for quite some time. We came up with a few
 approaches to implementing a better way to avoid redundant zonking. The
 key observation is that once we zonk `alpha` (and update its contents
 according to the current optimization), we don't have to do this again in
 the same zonk.

 a. We can track epoch numbers in the `TcM` monad (in a new mutable cell).
 The epoch would increase at every unification. Every `Indirect` node would
 store the epoch number of the type stored in the node -- that is, the type
 is fully zonked with respect to the stored epoch number. When zonking, if
 we encounter an `Indirect` whose epoch number matches the current epoch
 number, we know that the type is already zonked, and we can avoid
 traversing it.

 b. The idea in (a) doesn't apply only to filled-in metavariables, but to
 all types. The type-checker occasionally zonks types. However, if a type
 has already been zonked and there have been no unifications, then zonking
 it again is a waste of time. If we store an epoch number with every type,
 then we can check this against the global epoch number and skip some
 zonks.

 c. The idea in (b) is a bit heavy, though, requiring alternating proper
 `Type` nodes with epoch numbers in every type. Instead, we could just do
 this in `TcTyVar`s, where we store the epoch number of their kind.

 d. An alternative to epoch numbers is to have each individual zonk track
 which variables' contents are already zonked. This could be done by adding
 an `IORef TyVarEnv` to the local environment to the zonk (replacing the
 `()` environment of a `zonkTcType` or adding to the `ZonkEnv` of a
 `zonkTcTypeToType`). Every time we zonk a variable, add the variable to
 the env't, mapping it to its fully-zonked contents (or, in the case of a
 `TyVar`, a version of the `TyVar` with a zonked kind).

 With any of these ideas, it's not obvious that the work will be worth it,
 as it's hard to know how much redundant zonking we're doing.

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