Fix infinite loop in PredTYpe size checking (#5581)

1 files changed, 31 insertions, 6 deletions

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index f67df5a054..c362e62fe5 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1480,6 +1480,9 @@ checkValidInstance hs_type tyvars theta clas inst_tys
                  L loc _                          -> loc
 \end{code}
 
+Note [Paterson conditions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
 Termination test: the so-called "Paterson conditions" (see Section 5 of
 "Understanding functionsl dependencies via Constraint Handling Rules, 
 JFP Jan 2007).
@@ -1628,7 +1631,6 @@ fvTypes tys                = concat (map fvType tys)
 -- Size of a type: the number of variables and constructors
 sizeType :: Type -> Int
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
-sizeType ty | isPredTy ty  = sizePred ty
 sizeType (TyVarTy _)       = 1
 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
@@ -1638,18 +1640,41 @@ sizeType (ForAllTy _ ty)   = sizeType ty
 sizeTypes :: [Type] -> Int
 sizeTypes xs               = sum (map sizeType xs)
 
--- Size of a predicate
+-- Size of a predicate: the number of variables and constructors
+--
+-- Note [Paterson conditions on PredTypes]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 --
 -- We are considering whether *class* constraints terminate
--- Once we get into an implicit parameter or equality we
--- can't get back to a class constraint, so it's safe
--- to say "size 0".  See Trac #4200.
+-- (see Note [Paterson conditions]). Precisely, the Paterson conditions
+-- would have us check that "the constraint has fewer constructors and variables
+-- (taken together and counting repetitions) than the head.".
+--
+-- However, we can be a bit more refined by looking at which kind of constraint
+-- this actually is. There are two main tricks:
+--
+--  1. It seems like it should be OK not to count the tuple type constructor
+--     for a PredType like (Show a, Eq a) :: Constraint, since we don't
+--     count the "implicit" tuple in the ThetaType itself.
+--
+--     In fact, the Paterson test just checks *each component* of the top level
+--     ThetaType against the size bound, one at a time. By analogy, it should be
+--     OK to return the size of the *largest* tuple component as the size of the
+--     whole tuple.
+--
+--  2. Once we get into an implicit parameter or equality we
+--     can't get back to a class constraint, so it's safe
+--     to say "size 0".  See Trac #4200.
+--
+-- NB: we don't want to detect PredTypes in sizeType (and then call 
+-- sizePred on them), or we might get an infinite loop if that PredType
+-- is irreducible. See Trac #5581.
 sizePred :: PredType -> Int
 sizePred ty = go (predTypePredTree ty)
   where
     go (ClassPred _ tys') = sizeTypes tys'
     go (IPPred {})        = 0
     go (EqPred {})        = 0
-    go (TuplePred ts)     = sum (map go ts)
+    go (TuplePred ts)     = maximum (0:map go ts)
     go (IrredPred ty)     = sizeType ty
 \end{code}