Opened 5 years ago

Closed 3 years ago

Last modified 2 years ago

#7788 closed bug (fixed)

Recursive type family causes <<loop>>

Reported by: shachaf Owned by: goldfire
Priority: normal Milestone: 8.0.1
Component: Compiler (Type checker) Version: 7.6.2
Keywords: Cc: rwbarton@…, jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect result at runtime Test Case: indexed-types/should_fail/T7788
Blocked By: Blocking:
Related Tickets: #8550, #10079 Differential Rev(s):
Wiki Page:

Description

This file:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

data Proxy a = Proxy

foo :: Proxy (F (Fix Id)) -> ()
foo = undefined

newtype Fix a = Fix (a (Fix a))
newtype Id a = Id a

type family F a
type instance F (Fix a) = F (a (Fix a))
type instance F (Id a) = F a

main :: IO ()
main = print $ foo Proxy

Dies with <<loop>>. The type family is recursive, of course:

*Main> :kind! F (Fix Id)
F (Fix Id) :: *^CInterrupted.

But <<loop>> is still not the behavior I'd expect. The actual value is just undefined.

In the file that this example came up, the situation was even worse -- there was a situation where

moldMapOf l f = runAccessor . l (Accessor . f)
main = print $ (flip appEndo [] . moldMapOf (ix 3) (Endo . (:)) $ testVal :: [Int]) -- <<loop>>
main = print $ (flip appEndo [] . runAccessor . (ix 3) (Accessor . Endo . (:)) $ testVal :: [Int]) -- undefined

I.e. substitution can turn one program (which happens to be ⊥ here, admittedly, but that's not fundamental) into another (<<loop>>). This makes it very tricky to track down the recursive type family. If necessary I can hunt down a working test case and post it here -- it's a bit tricky to get working, though.

Change History (18)

comment:1 Changed 5 years ago by igloo

Component: CompilerCompiler (Type checker)
difficulty: Unknown
Milestone: 7.8.1
Owner: set to simonpj

Simon, is this the expected behaviour?

comment:2 Changed 4 years ago by rwbarton

Cc: rwbarton@… added

comment:3 Changed 4 years ago by thoughtpolice

Milestone: 7.8.37.10.1

Moving to 7.10.1

comment:4 Changed 3 years ago by thomie

Priority: normalhigh

The program from the description compiles fine with 7.8.3. GHC HEAD (ghc-7.9.20141121) however uses a huge amount of memory very quickly until I have to kill the process. It seems to never get past the Renamer/typechecker phase.

This looks like a regression, setting priority to high.

comment:5 Changed 3 years ago by simonpj

Does anyone actually care about programs with non-terminating type computations?

The type inference engine makes no claim to be a lazy evaluator. So if you write non-terminating type-level expressions, the compiler may loop.

I agree that it might be more puzzling if the compiler succeeds but the program loops at runtime. But that doesn't seem to be happening right now.

If this matters to anyone, sing out. Otherwise I'm going to leave it.

Simon

comment:6 Changed 3 years ago by goldfire

Here's what I'm worried about here.

This function is clearly very innocent:

id :: a -> a
id x = x

It compiles, obviously, without complaint.

But, with 7.10, the following doesn't:

type family F a where
  F a = F a

id2 :: F a -> F a
id2 x = x

This is slightly disturbing because id2 is merely a specialization of id.

I think there is an easy solution here, though: allow users to disable the optimisation that we've put into TcFlatten (try_to_reduce). If a user says -flazier-type-families, then we turn off the optimization. Most type-family-heavy programs will simply compile much more slowly... but a few will compile in finite time that didn't previously.

As a separate solution here, we probably should also detect when we're looping while evaluating a type family by tracking evaluation depth. I'd much rather get an error saying we've blown a limited stack size than to just loop.

comment:7 Changed 3 years ago by simonpj

I'm all for having an evaluation depth.

But I'm cautious about adding a flag. Just saying "lazier" doesn't say much. If we could somehow promise "lazy", for some well-specified meaning of that term, then I'd go for that. But not "disable some implementation optimisation that happens to allow one program (that one one cares about) to typecheck".

Currently we flatten type-function applications, and reduce them aggressively. I think it's pretty odd that id2 typechecks with the optimisation disabled; I strongly suspect that a simple variant will not.

Simon

comment:8 Changed 3 years ago by simonpj

Richard, for the evaluation-depth thing, I think that all that is necessary is:

  • Call bumpSubGoalDepth on the fe_loc field of fmode in try_to_reduce in TcFlatten.flatten_exact_fam_app_fully.
  • And call subGoalDepthExceeded in the same function.

Or the depth-exceeded check could be in flatten_one.

Might you do this?

Simon

comment:9 Changed 3 years ago by jstolarek

Cc: jstolarek added

comment:10 in reply to:  6 Changed 3 years ago by int-e

Replying to goldfire:

But, with 7.10, the following doesn't:

type family F a where
  F a = F a

id2 :: F a -> F a
id2 x = x

This is slightly disturbing because id2 is merely a specialization of id.

I think this is wrong: id2 does not have a type at all, and therefore does not specialize id.

The same is true for the original example. If one looks at the code generated by ghc-7.8.3, it tries to produce a witness for F (Fix Id) being a type, and foo checks that witness (which fails, producing the observed <<loop>>) before producing undefined:

-- core, with some non-essential parts omitted

cobox_rVz :: Main.F (Main.Fix Main.Id) ~ GHC.Prim.Any
cobox_rVz = cobox_rVz

foo :: Main.Proxy (Main.F (Main.Fix Main.Id)) -> ()
foo = case cobox_rVz of GHC.Types.Eq# _ -> undefined

That said it's unfortunate that GHC 7.10 loops rather than erroring out for these examples.

comment:11 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1
Priority: highnormal

Since this seems to be a regression, but also something of a corner case involving recursive type families, I'm pushing this one out to 7.12 and 'normal' priority (as 7.10 is feature complete).

comment:12 Changed 3 years ago by goldfire

Milestone: 7.12.17.10.1
Owner: changed from simonpj to goldfire

I just noticed that I had been asked to do this, and I think it would be nice in 7.10.

However, the fix would potentially be user-facing: A type-family-heavy program that compiles on 7.10.1RC2 might need to set -ftype-function-depth after the fix. Is that acceptable at this point?

Also, time is very precious for me before Feb. 27. I can get right on this Mar. 2.

(See also #8550, which is probably a dup of this bug.)

comment:13 Changed 3 years ago by goldfire

Just took a quick look at this, as I was in the area.

This will take some plumbing to implement right, sadly. The problem is that the type family reduction happens in the bowels of the flattening algorithm. To do this right, we need to update the CtLoc of the relevant constraint, but there's no good way to do that from the middle of the flattener.

Two ways forward:

  1. Install the plumbing. I vote that this should be a new FlatM monad (built on TcS) that allows updating of the CtLoc currently stored in the FlattenEnv. FlatM would gather up the FlattenEnv stuff, the runFlatten stuff, and this new type-family-depth-counting stuff. Seems like enough stuff to make it a new structure.
  1. Have a local counter just for the new, eager type family reduction. We have access to DynFlags, of course, so we can check if the number of eager reductions is more than requested. We can even add the number of eager reductions to the number of reductions done previously. What we can't do is record the number of eager reductions. So, if the stack depth were 200, then this plan (2) would allow, say, 190 eager reductions at one go, then some other solving, and then another 190 eager reductions, and then some solving, and so on. The depth is still bounded, but it makes it nigh impossible for a programmer to relate their choice of -ftype-function-depth to GHC's behavior, as it all depends on where the reduction takes place.

Thoughts?

Still no promises on getting to this for real before March, I'm afraid, especially for option 1.

comment:14 Changed 3 years ago by goldfire

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.
  1. Having FlatM modify a CtLoc is wrong, as it means that a certain CtEvidence suddenly has a new depth. This makes no sense.
  1. 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).
  1. rewriteEqEvidence checks for deriveds before reflexivity. These should be reversed.
  1. 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.
  1. 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.
  1. Setting the stack depths to 0 will serve as the marker for infinity.
  1. 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.
  1. 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.
  1. 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.

comment:15 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone.

comment:16 Changed 3 years ago by Richard Eisenberg <eir@…>

In c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa/ghc:

Do proper depth checking in the flattener to avoid looping.

This implements (roughly) the plan put forward in comment:14:ticket:7788,
fixing #7788, #8550, #9554, #10139, and addressing concerns raised in #10079.
There are some regressions w.r.t. GHC 7.8, but only with pathological type
families (like F a = F a). This also (hopefully -- don't have a test case)
fixes #10158. Unsolved problems include #10184 and #10185, which are both
known deficiencies of the approach used here.

As part of this change, the plumbing around detecting infinite loops has
changed. Instead of -fcontext-stack and -ftype-function-depth, we now have
one combined -freduction-depth parameter. Setting it to 0 disbales the
check, which is now the recommended way to get (terminating) code to
typecheck in releases. (The number of reduction steps may well change between
minor GHC releases!)

This commit also introduces a new IntWithInf type in BasicTypes
that represents an integer+infinity. This type is used in a few
places throughout the code.

Tests in
  indexed-types/should_fail/T7788
  indexed-types/should_fail/T8550
  indexed-types/should_fail/T9554
  indexed-types/should_compile/T10079
  indexed-types/should_compile/T10139
  typecheck/should_compile/T10184  (expected broken)
  typecheck/should_compile/T10185  (expected broken)

This commit also changes performance testsuite numbers, for the better.

comment:17 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T7788

comment:18 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

Note: See TracTickets for help on using tickets.