{-# LANGUAGE TypeFamilies #-}{-# LANGUAGE UndecidableInstances #-}data Proxy a = Proxyfoo :: Proxy (F (Fix Id)) -> ()foo = undefinednewtype Fix a = Fix (a (Fix a))newtype Id a = Id atype family F atype instance F (Fix a) = F (a (Fix a))type instance F (Id a) = F amain :: 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
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.
Trac metadata
Trac field
Value
Version
7.6.2
Type
Bug
TypeOfFailure
OtherFailure
Priority
normal
Resolution
Unresolved
Component
Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Child items
0
Show closed items
No child items are currently assigned. Use child items to break down this issue into smaller parts.
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.
type family F a where F a = F aid2 :: F a -> F aid2 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.
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.
type family F a whereF a = F aid2 :: F a -> F aid2 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 omittedcobox_rVz :: Main.F (Main.Fix Main.Id) ~ GHC.Prim.Anycobox_rVz = cobox_rVzfoo :: 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.
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).
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 (closed), which is probably a dup of this bug.)
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:
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.
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.
Just had a chat with Simon about all of this. We resolved several things:
The plumbing I have installed (in D653), using FlatM is helpful, and it caught errors in shortCutReduction.
Having FlatM modify a CtLoc is wrong, as it means that a certain CtEvidence suddenly has a new depth. This makes no sense.
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).
rewriteEqEvidence checks for deriveds before reflexivity. These should be reversed.
The flattener will count reductions separately from the canonicalizer. This amounts to plan (2) in ticket:7788#comment:96218, 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.
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.
Setting the stack depths to 0 will serve as the marker for infinity.
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.
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.
After all of this is done, it will be possible to move the newtype-unwrapping code into the flattener, with a depth check intact.