[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 simonpj):

 OK I finally understand what is going on.

 Suppose we have
 {{{
 alpha -> alpha
 where
   alpha is already unified:
     alpha := T{tc-tycon} Int -> Int
   and T is knot-tied
 }}}
 By "knot-tied" I mean that the occurrence of T is currently a `TcTyCon`,
 but the global env contains a mapping `"T" :-> T{knot-tied-tc}`.  See
 `Note [Type checking recursive type and class declarations]` in
 `TcTyClsDecls`.

 Now we call `zonkTcTypeToType` on that `alpha -> alpha`.

 * The first time we encounter `alpha` we invoke `TcHsTyn.zonkTyVarOcc`
 (because that's what the `tcm_tyvar` field of `zonk_tycomapper` says.
 Here's the code
 {{{
 zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
   | isTcTyVar tv
   = case tcTyVarDetails tv of
          SkolemTv {}    -> lookup_in_env
          RuntimeUnk {}  -> lookup_in_env
          MetaTv { mtv_ref = ref }
            -> do { cts <- readMutVar ref
                  ; case cts of
                       Flexi -> do { kind <- zonkTcTypeToType env
 (tyVarKind tv)
                                   ; zonk_unbound_tyvar (setTyVarKind tv
 kind) }
                       Indirect ty -> do { zty <- zonkTcTypeToType env ty
                                         -- Small optimisation: shortern-
 out indirect steps
                                         -- so that the old type may be
 more easily collected.
                                         ; writeMutVar ref (Indirect zty)
                                         ; return zty } }
 }}}

 * `zonkTyVarOcc` sees that the tyvar is already unifies (the `Indirect`
 branch), so it
   * zonks the type it points to `T{tc-tycon} Int -> Int`, yielding `T
 {knot-tied-tc} Int -> Int`
   * '''and updates `alpha` to point to this zonked type'''.

   The second step is a "small optimisation": there's no point in re-doing
 the work of zonking the type inside the `Indirect` if we encounter the
 variable a second time.

 * But alas, when we encounter `alpha` for a second time, we end up looking
 at `T{knot-tied-tc}` and fall into a black hole.  The whole point of
 `zonkTcTypeToType` is that it produces a type full of knot-tied tycons,
 and ''you must not look at the result''.

   To put it another way `zonkTcTypeToType . zonkTcTypeToType` is not the
 same as `zonkTcTypeToType`.  (If `zonkTcTypeToType` had different
 argumennt and result types, this issue would have been a type error; but
 the optimisation in `zonkTyVarOcc` would also become type-incorrect.)

 Now I see the problem, I'm astonished that it has not bitten us before.
 It shows up in #15552 in a more complicated way than the one I describe
 here, involving unification inside kinds.

 What to do?

 I think the Right Thing is probably to follow the thought experiment of
 distinguishing `Type` from `TcType`.  So then, instead of the current:
 {{{
 data MetaDetails
   = Flexi
   | Indirect TcType
 }}}
 we'd have so say
 {{{
 data MetaDetails
   = Flexi
   | IndirectTc TcType -- There may still be unification variables in here
   | Indirect   Type   -- No unification variables in here
 }}}
 This would mean that some 2-way branches become 3-way branches, so there
 might be a perf impact; I have no idea if it would be measurable.

 Interestingly, `zonkTcTypeToType` could stop altogether (hooray,
 efficient) when it finds `Indirect`, whereas `zonkTcType` can't (sigh),
 because it can't tell if an `IndirectTc` is from "this" zonk or some
 earlier one.   The only way I can see to solve that would be to count
 unifications, and record the current unification-count in the
 `IndirectTc`, thus `IndirectTc UnifCount TcType`.  That would of course
 carry its own costs.

 Any views?  I'm going to wait a few days before doing anything drastic
 here.

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