#7788: Recursive type family causes <<loop>> -------------------------------------+------------------------------------- Reporter: shachaf | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.6.2 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: Incorrect result | Test Case: at runtime | Blocking: Blocked By: | Differential Revisions: Related Tickets: #8550, #10079 | -------------------------------------+------------------------------------- Changes (by goldfire): * related: #8550 => #8550, #10079 Comment: Just had a chat with Simon about all of this. We resolved several things: 1. The plumbing I have installed (in Phab:D653), using `FlatM` is helpful, and it caught errors in `shortCutReduction`. 2. Having `FlatM` modify a `CtLoc` is wrong, as it means that a certain `CtEvidence` suddenly has a new depth. This makes no sense. 3. Simon was uncertain about the need to bump the stack depth in `rewriteEqEvidence`. But, after some thought, this is appropriate (in the non-reflexive case): `rewriteEqEvidence` is often called after some flattening, and it's quite possible that the flattening reduced some type families. We debated various schemes where we would bump only if the flattener did indeed reduce a type family (or newtype), and perhaps even bump by just the right number of reductions, but these didn't seem to work out. A central problem is what to do if we flatten, say, `Either (F a) (G b)` to `Either t1 t2`, where `F a` and `G b` took ''different'' numbers of steps to reduce. No handling of this scenario seemed adequate. So, we always bump (in the non-reflexive case). 4. `rewriteEqEvidence` checks for deriveds before reflexivity. These should be reversed. 5. The flattener will count reductions ''separately'' from the canonicalizer. This amounts to plan (2) in comment:13, where the flattener can take `-ftype-function-depth` steps during eager reduction. Then, regardless of the number of steps the flattener took, `rewriteEqEvidence` will bump only by one. So, the actual number of reductions possible is something like the product of the class stack depth and the type function depth. 6. Because of the point above, a programmer has no hope of setting these depths correctly when type families or newtypes reduce. Indeed, exactly when we hit a certain limit is quite likely to change between minor GHC releases. However, these limits are there only to prevent GHC from looping. Once a programmer has written their module, confirms that it compiles in finite time, it is safe just to disable these checks -- GHC will still never produce wrong code; it just might never produce any code at all. Thus, the new recommendation when a programmer hits these limits is just to disable the check. Disabling the check is infinitely more robust than choosing a new, arbitrary limit, likely to change between minor releases. 7. Setting the stack depths to 0 will serve as the marker for infinity. 8. There are other places where 0 means infinity, such as `st_max_ticks` in `SimplMonad.SimplTopEnv` and `TcValidity.TypeSize`. These should be abstracted into a new integer+infinity type, to go in `BasicTypes`. 9. `shortCutReduction` is utterly bogus, and it was a great surprise to Simon that the wheels haven't fallen off. We believe that this function must not be called at all during building GHC and in the testsuite. I will check this, and remove the function if it is unused. It can be fixed fairly easily. But as the name implies, it is simply an optimization. If it never triggers, then there's no reason to keep around taking up space. Simon conjectures that the reason it's not used is due to the new eager type family reduction in the flattener. 10. After all of this is done, it will be possible to move the newtype- unwrapping code into the flattener, with a depth check intact. The work above is expected to fix this ticket, #8550, and #10079. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/7788#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler