[GHC] #7788: Recursive type family causes <<loop>>

[GHC]

#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