#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