#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): It's not #15473. Here's a slightly cut down version {{{ {-# LANGUAGE DataKinds, ExistentialQuantification, GADTs, PolyKinds, TypeOperators #-} {-# LANGUAGE TypeInType, TypeFamilies #-} module T15552 where import Data.Kind data Elem :: k -> [k] -> Type data EntryOfVal (v :: Type) (kvs :: [Type]) where EntryOfVal :: forall (v :: Type) (kvs :: [Type]) (k :: Type). Elem (k, v) kvs -> EntryOfVal v kvs type family EntryOfValKey (eov :: EntryOfVal v kvs) :: Type type family GetEntryOfVal (eov :: EntryOfVal v kvs) :: Elem (EntryOfValKey eov, v) kvs type family FirstEntryOfVal (v :: Type) (kvs :: [Type]) :: EntryOfVal v kvs where FirstEntryOfVal v (_ : kvs) = 'EntryOfVal (GetEntryOfVal (FirstEntryOfVal v kvs)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15552#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 Simon Peyton Jones ): In [changeset:"184a569c5f5fe6e2eed73b2cff35722918c44efd/ghc" 184a569c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="184a569c5f5fe6e2eed73b2cff35722918c44efd" Clean up TcHsSyn.zonkEnv Triggered by Trac #15552, I'd been looking at ZonkEnv in TcHsSyn. This patch does some minor refactoring * Make ZonkEnv into a record with named fields, and use them. (I'm planning to add a new field, for TyCons, so this prepares the way.) * Replace UnboundTyVarZonker (a higer order function) with the simpler and more self-descriptive ZonkFlexi data type, below. It's just much more perspicuous and direct, and (I suspect) a tiny bit faster too -- no unknown function calls. data ZonkFlexi -- See Note [Un-unified unification variables] = DefaultFlexi -- Default unbound unificaiton variables to Any | SkolemiseFlexi -- Skolemise unbound unification variables -- See Note [Zonking the LHS of a RULE] | RuntimeUnkFlexi -- Used in the GHCi debugger There was one knock-on effect in the GHCi debugger -- the RuntimeUnkFlexi case. Somehow previously, these RuntimeUnk variables were sometimes getting SystemNames (and hence printed as 'a0', 'a1', etc) and sometimes not (and hence printed as 'a', 'b' etc). I'm not sure precisely why, but the new behaviour seems more uniform, so I just accepted the (small) renaming wibbles in some ghci.debugger tests. I had a quick look at perf: any changes are tiny. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15552#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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):

As for the larger plan: I like all of it

What is the "all of it" that you like, specifically? There are, I think, two pieces: 1. Eliminate the bug. How? Current brand leader: add a third contructor to `MetaDetails` (comment:3). Do we have any other alternatives on the table? 2. Clean up knot tying by using `ZonkEnv` (comment:4). This is pure refactoring, and hence not urgent, but it smells right to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15552#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#15552: Infinite loop/panic with an existential type. -------------------------------------+------------------------------------- Reporter: howtonotwin | Owner: (none) Type: bug | Status: merge 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: OK I think I'm done with this. Perf is fine; and the bug is fixed. Lots of Notes to explain. It fixes an outright bug, so merge if poss. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15552#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler