Allow recursive (undecidable) superclasses
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 15 Dec 2015 14:26:13 +0000 (14:26 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 15 Dec 2015 14:33:32 +0000 (14:33 +0000)
This patch fulfils the request in Trac #11067, #10318, and #10592,
by lifting the conservative restrictions on superclass constraints.

These restrictions are there (and have been since Haskell was born) to
ensure that the transitive superclasses of a class constraint is a finite
set.  However (a) this restriction is conservative, and can be annoying
when there really is no recursion, and (b) sometimes genuinely recursive
superclasses are useful (see the tickets).

Dimitrios and I worked out that there is actually a relatively simple way
to do the job. It’s described in some detail in

   Note [The superclass story] in TcCanonical
   Note [Expanding superclasses] in TcType

In brief, the idea is to expand superclasses only finitely, but to
iterate (using a loop that already existed) if there are more
superclasses to explore.

Other small things

- I improved grouping of error messages a bit in TcErrors

- I re-centred the haddock.compiler test, which was at 9.8%
  above the norm, and which this patch pushed slightly over

57 files changed:
compiler/main/DynFlags.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/utils/Bag.hs
docs/users_guide/glasgow_exts.rst
libraries/ghc-prim/GHC/Classes.hs
testsuite/tests/ado/ado004.stderr
testsuite/tests/driver/T4437.hs
testsuite/tests/ghci/scripts/ghci013.stdout
testsuite/tests/indexed-types/should_compile/T10318.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T11067.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_compile/T3208b.stderr
testsuite/tests/indexed-types/should_compile/T8889.stderr
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T1897b.stderr
testsuite/tests/indexed-types/should_fail/T3330a.stderr
testsuite/tests/indexed-types/should_fail/T4174.stderr
testsuite/tests/indexed-types/should_fail/T8227.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/module/mod40.stderr
testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
testsuite/tests/partial-sigs/should_fail/T10999.stderr
testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
testsuite/tests/perf/haddock/all.T
testsuite/tests/pmcheck/should_compile/T3927b.hs
testsuite/tests/polykinds/T7332.hs
testsuite/tests/polykinds/T7594.hs
testsuite/tests/polykinds/T7594.stderr
testsuite/tests/polykinds/T9017.stderr
testsuite/tests/simplCore/should_compile/T4398.stderr
testsuite/tests/typecheck/should_compile/T10100.hs
testsuite/tests/typecheck/should_compile/T10109.hs
testsuite/tests/typecheck/should_compile/T10564.hs
testsuite/tests/typecheck/should_compile/T9834.stderr
testsuite/tests/typecheck/should_compile/tc256.hs
testsuite/tests/typecheck/should_fail/T2714.stderr
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/T7869.stderr
testsuite/tests/typecheck/should_fail/T8883.stderr
testsuite/tests/typecheck/should_fail/T9415.stderr
testsuite/tests/typecheck/should_fail/T9739.stderr
testsuite/tests/typecheck/should_fail/tcfail027.stderr
testsuite/tests/typecheck/should_fail/tcfail216.hs
testsuite/tests/typecheck/should_fail/tcfail216.stderr
testsuite/tests/typecheck/should_fail/tcfail217.hs
testsuite/tests/typecheck/should_fail/tcfail217.stderr

index 98a3631..6372918 100644 (file)
@@ -565,6 +565,7 @@ data ExtensionFlag
    | Opt_OverlappingInstances
    | Opt_UndecidableInstances
    | Opt_IncoherentInstances
+   | Opt_UndecidableSuperClasses
    | Opt_MonomorphismRestriction
    | Opt_MonoPatBinds
    | Opt_MonoLocalBinds
@@ -3261,6 +3262,7 @@ xFlags = [
   flagSpec "TypeSynonymInstances"             Opt_TypeSynonymInstances,
   flagSpec "UnboxedTuples"                    Opt_UnboxedTuples,
   flagSpec "UndecidableInstances"             Opt_UndecidableInstances,
+  flagSpec "UndecidableSuperClasses"          Opt_UndecidableSuperClasses,
   flagSpec "UnicodeSyntax"                    Opt_UnicodeSyntax,
   flagSpec "UnliftedFFITypes"                 Opt_UnliftedFFITypes,
   flagSpec "ViewPatterns"                     Opt_ViewPatterns
index 7ac2a9a..4edc312 100644 (file)
@@ -3,7 +3,7 @@
 module TcCanonical(
      canonicalize,
      unifyDerived,
-
+     makeSuperClasses, mkGivensWithSuperClasses,
      StopOrContinue(..), stopWith, continueWith
   ) where
 
@@ -27,6 +27,7 @@ import OccName( OccName )
 import Outputable
 import DynFlags( DynFlags )
 import VarSet
+import NameSet
 import RdrName
 
 import Pair
@@ -147,11 +148,11 @@ canonicalize ct@(CNonCanonical { cc_ev = ev })
        ; {-# SCC "canEvVar" #-}
          canEvNC ev }
 
-canonicalize (CDictCan { cc_ev = ev
-                       , cc_class  = cls
-                       , cc_tyargs = xis })
+canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
+                       , cc_tyargs = xis, cc_pend_sc = pend_sc })
   = {-# SCC "canClass" #-}
-    canClass ev cls xis -- Do not add any superclasses
+    canClass ev cls xis pend_sc
+
 canonicalize (CTyEqCan { cc_ev = ev
                        , cc_tyvar  = tv
                        , cc_rhs    = xi
@@ -191,59 +192,118 @@ canEvNC ev
 ************************************************************************
 -}
 
-canClass, canClassNC
-   :: CtEvidence
-   -> Class -> [Type] -> TcS (StopOrContinue Ct)
+canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
+canClassNC ev cls tys = canClass ev cls tys (has_scs cls)
+  where
+    has_scs cls = not (null (classSCTheta cls))
 
--- The canClassNC version is used on non-canonical constraints
--- and adds superclasses.  The plain canClass version is used
--- for already-canonical class constraints (but which might have
--- been subsituted or somthing), and hence do not need superclasses
-
-canClassNC ev cls tys
-  = canClass ev cls tys
-    `andWhenContinue` emitSuperclasses
+canClass :: CtEvidence -> Class -> [Type] -> Bool -> TcS (StopOrContinue Ct)
+-- Precondition: EvVar is class evidence
 
-canClass ev cls tys
+canClass ev cls tys pend_sc
   =   -- all classes do *nominal* matching
     ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
     do { (xis, cos) <- flattenManyNom ev tys
        ; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
              xi = mkClassPred cls xis
              mk_ct new_ev = CDictCan { cc_ev = new_ev
-                                     , cc_tyargs = xis, cc_class = cls }
+                                     , cc_tyargs = xis
+                                     , cc_class = cls
+                                     , cc_pend_sc = pend_sc }
        ; mb <- rewriteEvidence ev xi co
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
        ; return (fmap mk_ct mb) }
 
-emitSuperclasses :: Ct -> TcS (StopOrContinue Ct)
-emitSuperclasses ct@(CDictCan { cc_ev = ev , cc_tyargs = xis_new, cc_class = cls })
-            -- Add superclasses of this one here, See Note [Adding superclasses].
-            -- But only if we are not simplifying the LHS of a rule.
- = do { newSCWorkFromFlavored ev cls xis_new
-      -- Arguably we should "seq" the coercions if they are derived,
-      -- as we do below for emit_kind_constraint, to allow errors in
-      -- superclasses to be executed if deferred to runtime!
-      ; continueWith ct }
-emitSuperclasses _ = panic "emit_superclasses of non-class!"
-
-{- Note [Adding superclasses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Since dictionaries are canonicalized only once in their lifetime, the
-place to add their superclasses is canonicalisation.  See Note [Add
-superclasses only during canonicalisation].  Here is what we do:
-
-  Givens:   Add all their superclasses as Givens.
-            They may be needed to prove Wanteds.
-
-  Wanteds/Derived:
-            Add all their superclasses as Derived.
-            The sole reason is to expose functional dependencies
-            in superclasses or equality superclasses.
-
-Examples of how adding superclasses as Derived is useful
+{- Note [The superclass story]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We need to add superclass constraints for two reasons:
+
+* For givens, they give us a route to to proof.  E.g.
+    f :: Ord a => a -> Bool
+    f x = x == x
+  We get a Wanted (Eq a), which can only be solved from the superclass
+  of the Given (Ord a).
+
+* For wanteds, they may give useful functional dependencies.  E.g.
+     class C a b | a -> b where ...
+     class C a b => D a b where ...
+  Now a Wanted constraint (D Int beta) has (C Int beta) as a superclass
+  and that might tell us about beta, via C's fundeps.  We can get this
+  by generateing a Derived (C Int beta) constraint.  It's derived because
+  we don't actually have to cough up any evidence for it; it's only there
+  to generate fundep equalities.
+
+See Note [Why adding superclasses can help].
+
+For these reasons we want to generate superclass constraints for both
+Givens and Wanteds. But:
+
+* (Minor) they are often not needed, so generating them aggressively
+  is a waste of time.
+
+* (Major) if we want recursive superclasses, there would be an infinite
+  number of them.  Here is a real-life example (Trac #10318);
+
+     class (Frac (Frac a) ~ Frac a,
+            Fractional (Frac a),
+            IntegralDomain (Frac a))
+         => IntegralDomain a where
+      type Frac a :: *
+
+  Notice that IntegralDomain has an associated type Frac, and one
+  of IntegralDomain's superclasses is another IntegralDomain constraint.
+
+So here's the plan:
+
+1. Generate superclasses for given (but not wanted) constraints;
+   see Note [Aggressively expand given superclasses].  However
+   stop if you encounter the same class twice.  That is, expand
+   eagerly, but have a conservative termination condition: see
+   Note [Expanding superclasses] in TcType.
+
+2. Solve the wanteds as usual, but do /no/ expansion of superclasses
+   in solveSimpleGivens or solveSimpleWanteds.
+   See Note [Danger of adding superclasses during solving]
+
+3. If we have any remaining unsolved wanteds, try harder:
+   take both the Givens and Wanteds, and expand superclasses again.
+   This may succeed in generating (a finite number of) extra Givens,
+   and extra Deriveds. Both may help the proof.
+   This is done in TcSimplify.expandSuperClasses.
+
+4. Go round to (2) again.  This loop (2,3,4) is implemented
+   in TcSimplify.simpl_loop.
+
+We try to terminate the loop by flagging which class constraints
+(given or wanted) are potentially un-expanded.  This is what the
+cc_pend_sc flag is for in CDictCan.  So in Step 3 we only expand
+superclasses for constraints with cc_pend_sc set to true (i.e.
+isPendingScDict holds).
+
+When we take a CNonCanonical or CIrredCan, but end up classifying it
+as a CDictCan, we set the cc_pend_sc flag to False.
+
+Note [Aggressively expand given superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In step (1) of Note [The superclass story], why do we aggressively
+expand Given superclasses by one layer?  Mainly because of some very
+obscure cases like this:
+
+   instance Bad a => Eq (T a)
+
+   f :: (Ord (T a)) => blah
+   f x = ....needs Eq (T a), Ord (T a)....
+
+Here if we can't satisfy (Eq (T a)) from the givens we'll use the
+instance declaration; but then we are stuck with (Bad a).  Sigh.
+This is really a case of non-confluent proofs, but to stop our users
+complaining we expand one layer in advance.
+
+Note [Why adding superclasses can help]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Examples of how adding superclasses can help:
 
     --- Example 1
         class C a b | a -> b
@@ -280,34 +340,8 @@ Examples of how adding superclasses as Derived is useful
       [D] beta ~ b
     which is what we want.
 
----------- Historical note -----------
-Example of why adding superclass of a Wanted as a Given would
-be terrible, see Note [Do not add superclasses of solved dictionaries]
-in TcSMonad, which has this example:
-        class Ord a => C a where
-        instance Ord [a] => C [a] where ...
-Suppose we are trying to solve
-  [G] d1 : Ord a
-  [W] d2 : C [a]
-If we (bogusly) added the superclass of d2 as Given we'd have
-  [G] d1 : Ord a
-  [W] d2 : C [a]
-  [G] d3 : Ord [a]   -- Superclass of d2, bogus
-
-Then we'll use the instance decl to give
-  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d4
-  [G] d3 : Ord [a]   -- Superclass of d2, bogus
-  [W] d4: Ord [a]
-
-And now we could bogusly solve d4 from d3.
----------- End of historical note -----------
-
-Note [Add superclasses only during canonicalisation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We add superclasses only during canonicalisation, on the passage
-from CNonCanonical to CDictCan.  A class constraint can be repeatedly
-rewritten, and there's no point in repeatedly adding its superclasses.
-
+Note [Danger of adding superclasses during solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Here's a serious, but now out-dated example, from Trac #4497:
 
    class Num (RealOf t) => Normed t
@@ -334,27 +368,70 @@ Mind you, now that Wanteds cannot rewrite Derived, I think this particular
 situation can't happen.
   -}
 
-newSCWorkFromFlavored :: CtEvidence -> Class -> [Xi] -> TcS ()
--- Returns superclasses, see Note [Adding superclasses]
-newSCWorkFromFlavored flavor cls xis
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- flavor
-  = do { given_evs <- newGivenEvVars (mk_given_loc loc)
-                                     (mkEvScSelectors (EvId evar) cls xis)
-       ; emitWorkNC given_evs }
+mkGivensWithSuperClasses :: CtLoc -> [EvId] -> TcS [Ct]
+-- From a given EvId, make its Ct, plus the Ct's of its superclasses
+-- See Note [The superclass story]
+-- The loop-breaking here follows Note [Expanding superclasses] in TcType
+mkGivensWithSuperClasses loc ev_ids = concatMapM go ev_ids
+  where
+    go ev_id = mk_superclasses emptyNameSet $
+               CtGiven { ctev_evar = ev_id
+                       , ctev_pred = evVarPred ev_id
+                       , ctev_loc  = loc }
+
+makeSuperClasses :: [Ct] -> TcS [Ct]
+-- Returns strict superclasses, transitively, see Note [The superclasses story]
+-- See Note [The superclass story]
+-- The loop-breaking here follows Note [Expanding superclasses] in TcType
+makeSuperClasses cts = concatMapM go cts
+  where
+    go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
+          = mk_strict_superclasses emptyNameSet ev cls tys
+    go ct = pprPanic "makeSuperClasses" (ppr ct)
+
+mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
+-- Return this constraint, plus its superclasses, if any
+mk_superclasses rec_clss ev
+  | ClassPred cls tys <- classifyPredType (ctEvPred ev)
+  = mk_superclasses_of rec_clss ev cls tys
+
+  | otherwise   -- Superclass is not a class predicate
+  = return [mkNonCanonical ev]
+
+mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
+-- Return this class constraint, plus its superclasses
+mk_superclasses_of rec_clss ev cls tys
+  | loop_found
+  = return [this_ct]
+  | otherwise
+  = do { sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
+       ; return (this_ct : sc_cts) }
+  where
+    cls_nm     = className cls
+    loop_found = cls_nm `elemNameSet` rec_clss
+    rec_clss'  | isCTupleClass cls = rec_clss  -- Never contribute to recursion
+               | otherwise         = rec_clss `extendNameSet` cls_nm
+    this_ct    = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
+                          , cc_pend_sc = loop_found }
+
+mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
+mk_strict_superclasses rec_clss ev cls tys
+  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
+  = do { sc_evs <- newGivenEvVars (mk_given_loc loc)
+                                  (mkEvScSelectors (EvId evar) cls tys)
+       ; concatMapM (mk_superclasses rec_clss) sc_evs }
 
-  | isEmptyVarSet (tyCoVarsOfTypes xis)
-  = return () -- Wanteds with no variables yield no deriveds.
+
+  | isEmptyVarSet (tyCoVarsOfTypes tys)
+  = return [] -- Wanteds with no variables yield no deriveds.
               -- See Note [Improvement from Ground Wanteds]
 
   | otherwise -- Wanted/Derived case, just add those SC that can lead to improvement.
-  = do { let sc_rec_theta = transSuperClasses cls xis
-             impr_theta   = filter isImprovementPred sc_rec_theta
-             loc          = ctEvLoc flavor
-       ; traceTcS "newSCWork/Derived" $ text "impr_theta =" <+> ppr impr_theta
-       ; emitNewDeriveds loc impr_theta }
-
+  = do { let loc = ctEvLoc ev
+       ; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
+       ; concatMapM (mk_superclasses rec_clss) sc_evs }
   where
-    size = sizeTypes xis
+    size = sizeTypes tys
     mk_given_loc loc
        | isCTupleClass cls
        = loc   -- For tuple predicates, just take them apart, without
@@ -373,6 +450,8 @@ newSCWorkFromFlavored flavor cls xis
        | otherwise  -- Probably doesn't happen, since this function
        = loc        -- is only used for Givens, but does no harm
 
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1876,3 +1955,4 @@ unify_derived loc role    orig_ty1 orig_ty2
 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
 maybeSym IsSwapped  co = mkTcSymCo co
 maybeSym NotSwapped co = co
+
index 94cd9ad..e23c750 100644 (file)
@@ -345,7 +345,7 @@ warnRedundantConstraints ctxt env info ev_vars
                      _        -> ev_vars
 
    improving ev_var = any isImprovementPred $
-                      transSuperClassesPred (idType ev_var)
+                      transSuperClasses (idType ev_var)
 
 {- Note [Redundant constraints in instance decls]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -406,8 +406,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
                                                   True, mkUserTypeErrorReporter)
               , ("insoluble1",   is_given_eq,     True, mkGroupReporter mkEqErr)
               , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
-              , ("insoluble3",   rigid_nom_tv_eq, True, mkSkolReporter)
-              , ("insoluble4",   rigid_nom_eq,    True, mkGroupReporter mkEqErr)
+              , ("skolem eq1",   very_wrong,      True, mkSkolReporter)
+              , ("skolem eq2",   skolem_eq,       True, mkSkolReporter)
+              , ("non-tv eq",    non_tv_eq,       True, mkSkolReporter)
               , ("Out of scope", is_out_of_scope, True,  mkHoleReporter)
               , ("Holes",        is_hole,         False, mkHoleReporter)
 
@@ -420,28 +421,41 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
               , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)
               , ("Dicts",           is_dict,         False, mkGroupReporter mkDictErr) ]
 
-    rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict,
+    -- rigid_nom_eq, rigid_nom_tv_eq,
+    is_hole, is_dict,
       is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
 
-    utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
-    utterly_wrong _ _                      = False
-
-    is_out_of_scope ct _ = isOutOfScopeCt ct
-    is_hole         ct _ = isHoleCt ct
-
     is_given_eq ct pred
        | EqPred {} <- pred = arisesFromGivens ct
        | otherwise         = False
        -- I think all given residuals are equalities
 
-    is_user_type_error ct _ = isUserTypeErrorCt ct
+    -- Things like (Int ~N Bool)
+    utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
+    utterly_wrong _ _                      = False
+
+    -- Things like (a ~N Int)
+    very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
+    very_wrong _ _                      = False
+
+    -- Things like (a ~N b) or (a  ~N  F Bool)
+    skolem_eq _ (EqPred NomEq ty1 _) =  isSkolemTy tc_lvl ty1
+    skolem_eq _ _                    = False
 
-    -- Skolem (i.e. non-meta) type variable on the left
-    rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
+    -- Things like (F a  ~N  Int)
+    non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
+    non_tv_eq _ _                    = False
 
-    rigid_nom_tv_eq _ pred
-      | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
-      | otherwise              = False
+--    rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
+--
+--    rigid_nom_tv_eq _ pred
+--      | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
+--      | otherwise              = False
+
+    is_out_of_scope ct _ = isOutOfScopeCt ct
+    is_hole         ct _ = isHoleCt ct
+
+    is_user_type_error ct _ = isUserTypeErrorCt ct
 
     is_equality _ (EqPred {}) = True
     is_equality _ _           = False
@@ -457,6 +471,15 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
 
 
 ---------------
+isSkolemTy :: TcLevel -> Type -> Bool
+isSkolemTy tc_lvl ty
+  = case getTyVar_maybe ty of
+      Nothing -> False
+      Just tv -> isSkolemTyVar tv
+              || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
+         -- The latter case is for touchable SigTvs
+         -- we postpone untouchables to a latter test (too obscure)
+
 isTyFun_maybe :: Type -> Maybe TyCon
 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
                       Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
@@ -476,15 +499,19 @@ type ReporterSpec
     , Reporter)                  -- The reporter itself
 
 mkSkolReporter :: Reporter
--- Suppress duplicates with the same LHS
+-- Suppress duplicates with either the same LHS, or same location
 mkSkolReporter ctxt cts
-  = mapM_ (reportGroup mkEqErr ctxt) (equivClasses cmp_lhs_type cts)
+  = mapM_ (reportGroup mkEqErr ctxt) (group cts)
   where
-    cmp_lhs_type ct1 ct2
-      = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
-           (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
-             (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
-           _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
+     group [] = []
+     group (ct:cts) = (ct : yeses) : group noes
+        where
+          (yeses, noes) = partition (group_with ct) cts
+
+     group_with ct1 ct2
+       | EQ <- cmp_loc      ct1 ct2 = True
+       | EQ <- cmp_lhs_type ct1 ct2 = True
+       | otherwise                  = False
 
 mkHoleReporter :: Reporter
 -- Reports errors one at a time
@@ -515,7 +542,16 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
 mkGroupReporter mk_err ctxt cts
   = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
   where
-    cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
+
+cmp_lhs_type :: Ct -> Ct -> Ordering
+cmp_lhs_type ct1 ct2
+  = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
+       (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
+         (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
+       _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
+
+cmp_loc :: Ct -> Ct -> Ordering
+cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2)
 
 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
             -> [Ct] -> TcM ()
index c78d6bb..c044d20 100644 (file)
@@ -1,7 +1,7 @@
 {-# LANGUAGE CPP #-}
 
 module TcInteract (
-     solveSimpleGivens,   -- Solves [EvVar],GivenLoc
+     solveSimpleGivens,   -- Solves [Ct]
      solveSimpleWanteds,  -- Solves Cts
 
      solveCallStack,      -- for use in TcSimplify
@@ -132,24 +132,18 @@ that prepareInertsForImplications will discard the insolubles, so we
 must keep track of them separately.
 -}
 
-solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts
--- Solves the givens, adding them to the inert set
--- Returns any insoluble givens, which represent inaccessible code,
--- taking those ones out of the inert set
-solveSimpleGivens loc givens
+solveSimpleGivens :: [Ct] -> TcS Cts
+solveSimpleGivens givens
   | null givens  -- Shortcut for common case
   = return emptyCts
   | otherwise
-  = do { go (map mk_given_ct givens)
+  = do { go givens
        ; takeGivenInsolubles }
   where
-    mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
-                                                , ctev_pred = evVarPred ev_id
-                                                , ctev_loc  = loc })
     go givens = do { solveSimples (listToBag givens)
                    ; new_givens <- runTcPluginsGiven
-                   ; when (notNull new_givens) (go new_givens)
-                   }
+                   ; when (notNull new_givens) $
+                     go new_givens }
 
 solveSimpleWanteds :: Cts -> TcS WantedConstraints
 -- NB: 'simples' may contain /derived/ equalities, floated
index 94b7478..a6a6fa1 100644 (file)
@@ -81,7 +81,7 @@ module TcRnTypes(
         toDerivedWC,
         andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
-        isDroppableDerivedLoc, insolubleImplic, trulyInsoluble,
+        isDroppableDerivedLoc, insolubleImplic,
         arisesFromGivens,
 
         Implication(..), ImplicStatus(..), isInsolubleStatus,
@@ -1339,7 +1339,13 @@ data Ct
   = CDictCan {  -- e.g.  Num xi
       cc_ev     :: CtEvidence, -- See Note [Ct/evidence invariant]
       cc_class  :: Class,
-      cc_tyargs :: [Xi]        -- cc_tyargs are function-free, hence Xi
+      cc_tyargs :: [Xi],       -- cc_tyargs are function-free, hence Xi
+      cc_pend_sc :: Bool       -- True <=> (a) cc_class has superclasses
+                               --          (b) we have not yet added those
+                               --              superclasses as Givens
+           -- NB: cc_pend_sc is used for G/W/D.  For W/D the reason
+           --     we need superclasses is to expose possible improvement
+           --     via fundeps
     }
 
   | CIrredEvCan {  -- These stand for yet-unusable predicates
@@ -1872,11 +1878,11 @@ trulyInsoluble :: TcLevel -> Ct -> Bool
 -- The constraint is in the wc_insol set,
 -- but we do not treat as truly isoluble
 --  a) type-holes, arising from PartialTypeSignatures,
---  b) an out-of-scope variable
+--     (except out-of-scope variables masquerading as type-holes)
 -- Yuk!
-trulyInsoluble tc_lvl insol
-   isOutOfScopeCt insol
-  || isRigidEqPred tc_lvl (classifyPredType (ctPred insol))
+trulyInsoluble _tc_lvl insol
+  | CHoleCan {} <- insol = isOutOfScopeCt insol
+  | otherwise            = True
 
 instance Outputable WantedConstraints where
   ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
index 1cc7533..ac38e17 100644 (file)
@@ -51,7 +51,7 @@ module TcSMonad (
     emptyInert, getTcSInerts, setTcSInerts, takeGivenInsolubles,
     matchableGivens, prohibitedSuperClassSolve,
     getUnsolvedInerts,
-    removeInertCts,
+    removeInertCts, getPendingScDicts, isPendingScDict,
     addInertCan, addInertEq, insertFunEq,
     emitInsoluble, emitWorkNC, emitWorkCt,
 
@@ -558,9 +558,7 @@ data InertCans   -- See Note [Detailed InertCans Invariants] for more
               --   (b) emitDerivedShadows
 
        , inert_dicts :: DictMap Ct
-              -- Dictionaries only, index is the class
-              -- NB: index is /not/ the whole type because FD reactions
-              -- need to match the class but not necessarily the whole type.
+              -- Dictionaries only
 
        , inert_safehask :: DictMap Ct
               -- Failed dictionary resolution due to Safe Haskell overlapping
@@ -1568,7 +1566,7 @@ After solving the Givens we take two things out of the inert set
 
   a) The insolubles; we return these to report inaccessible code
      We return these separately.  We don't want to leave them in
-     the inert set, lest we onfuse them with insolubles arising from
+     the inert set, lest we confuse them with insolubles arising from
      solving wanteds
 
   b) Any Derived CFunEqCans.  Derived CTyEqCans are in the
@@ -1633,6 +1631,35 @@ getInertGivens
                      $ concat (varEnvElts (inert_eqs inerts))
        ; return (filter isGivenCt all_cts) }
 
+getPendingScDicts :: TcS [Ct]
+-- Find all inert Given dictionaries whose cc_pend_sc flag is True
+-- Set the flag to False in the inert set, and return that Ct
+getPendingScDicts = updRetInertCans get_sc_dicts
+  where
+    get_sc_dicts ic@(IC { inert_dicts = dicts })
+      = (sc_pend_dicts, ic')
+      where
+        ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
+
+        sc_pend_dicts :: [Ct]
+        sc_pend_dicts = foldDicts get_pending dicts []
+
+    get_pending :: Ct -> [Ct] -> [Ct]  -- Get dicts with cc_pend_sc = True
+                                       -- but flipping the flag
+    get_pending dict dicts
+        | Just dict' <- isPendingScDict dict = dict' : dicts
+        | otherwise                          = dicts
+
+    add :: Ct -> DictMap Ct -> DictMap Ct
+    add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts
+        = addDict dicts cls tys ct
+    add ct _ = pprPanic "getPendingScDicts" (ppr ct)
+
+isPendingScDict :: Ct -> Maybe Ct
+isPendingScDict ct@(CDictCan { cc_pend_sc = True })
+                  = Just (ct { cc_pend_sc = False })
+isPendingScDict _ = Nothing
+
 getUnsolvedInerts :: TcS ( Bag Implication
                          , Cts     -- Tyvar eqs: a ~ ty
                          , Cts     -- Fun eqs:   F a ~ ty
index 261abd0..c6aae95 100644 (file)
@@ -31,6 +31,7 @@ import PrelNames
 import TcErrors
 import TcEvidence
 import TcInteract
+import TcCanonical   ( makeSuperClasses, mkGivensWithSuperClasses )
 import TcMType   as TcM
 import TcRnMonad as TcM
 import TcSMonad  as TcS
@@ -422,18 +423,36 @@ simplifyDefault theta
 ------------------
 tcCheckSatisfiability :: Bag EvVar -> TcM Bool
 -- Return True if satisfiable, False if definitely contradictory
-tcCheckSatisfiability givens
+tcCheckSatisfiability given_ids
   = do { lcl_env <- TcM.getLclEnv
        ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
-       ; traceTc "checkSatisfiability {" (ppr givens)
        ; (res, _ev_binds) <- runTcS $
-             do { cts <- solveSimpleGivens given_loc (bagToList givens)
-                ; return (not (isEmptyBag cts)) }
-       ; traceTc "checkSatisfiability }" (ppr res)
-       ; return (not res) }
-
-{-
-*********************************************************************************
+             do { traceTcS "checkSatisfiability {" (ppr given_ids)
+                ; given_cts <- mkGivensWithSuperClasses given_loc (bagToList given_ids)
+                     -- Need their superclasses, because (Int ~ Bool) has (Int ~~ Bool)
+                     -- as a superclass, and it's the latter that is insoluble
+                ; insols <- solveSimpleGivens given_cts
+                ; insols <- try_harder insols
+                ; traceTcS "checkSatisfiability }" (ppr insols)
+                ; return (isEmptyBag insols) }
+       ; return res }
+  where
+    try_harder :: Cts -> TcS Cts
+    -- Maybe we have to search up the superclass chain to find
+    -- an unsatisfiable constraint.  Example: pmcheck/T3927b.
+    try_harder insols
+      | not (isEmptyBag insols)   -- We've found that it's definitely unsatisfiable
+      = return insols             -- Hurrah -- stop now.
+      | otherwise
+      = do { pending_given <- getPendingScDicts
+           ; new_given <- makeSuperClasses pending_given
+           ; if null new_given     -- No new superclasses to try, so no point
+             then return emptyBag  --                             in continuing
+             else                  -- Some new superclasses; have a go
+        do { insols <- solveSimpleGivens new_given
+           ; try_harder insols } }
+
+{- ********************************************************************************
 *                                                                                 *
 *                            Inference
 *                                                                                 *
@@ -971,12 +990,13 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
          -- of adding Derived insolubles twice; see
          -- TcSMonad Note [Do not add duplicate derived insolubles]
        ; wc1 <- solveSimpleWanteds simples
+       ; (no_new_scs, wc1) <- expandSuperClasses wc1
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
 
        ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
 
        ; dflags <- getDynFlags
-       ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
+       ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs no_new_scs
                                 (WC { wc_simple = simples1, wc_impl = implics2
                                     , wc_insol  = insols `unionBags` insols1 })
 
@@ -987,10 +1007,10 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
 
        ; return final_wc }
 
-simpl_loop :: Int -> IntWithInf -> Cts
+simpl_loop :: Int -> IntWithInf -> Cts -> Bool
            -> WantedConstraints
            -> TcS WantedConstraints
-simpl_loop n limit floated_eqs
+simpl_loop n limit floated_eqs no_new_given_scs
            wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   | n `intGtLimit` limit
   = failTcS (hang (ptext (sLit "solveWanteds: too many iterations")
@@ -998,7 +1018,7 @@ simpl_loop n limit floated_eqs
                 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
                         , ppr wc ] ))
 
-  | no_floated_eqs
+  | isEmptyBag floated_eqs && no_new_given_scs
   = return wc  -- Done!
 
   | otherwise
@@ -1011,19 +1031,42 @@ simpl_loop n limit floated_eqs
                                -- NB: the floated_eqs may include /derived/ equalities
                                --     arising from fundeps inside an implication
 
+       ; (no_new_scs, wc1) <- expandSuperClasses wc1
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
 
-       -- solveImplications may make progress only if unifs2 holds
+       -- We have already tried to solve the nested implications once
+       -- Try again only if we have unified some meta-variables
+       -- (which is a bit like adding more givens
+       -- See Note [Cutting off simpl_loop]
        ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
                                      then return (emptyBag, implics)
                                      else solveNestedImplications (implics `unionBags` implics1)
 
-       ; simpl_loop (n+1) limit floated_eqs2
+       ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
                     (WC { wc_simple = simples1, wc_impl = implics2
                         , wc_insol  = insols `unionBags` insols1 }) }
 
-  where
-    no_floated_eqs = isEmptyBag floated_eqs
+expandSuperClasses :: WantedConstraints -> TcS (Bool, WantedConstraints)
+-- If there are any unsolved wanteds, expand one step of superclasses for
+-- unsolved wanteds or givens
+-- See Note [The superclass story] in TcCanonical
+expandSuperClasses wc@(WC { wc_simple = unsolved, wc_insol = insols })
+  | isEmptyBag unsolved  -- No unsolved simple wanteds, so do not add suerpclasses
+  = return (True, wc)
+  | otherwise
+  = do { let (pending_wanted, unsolved') = mapAccumBagL get [] unsolved
+             get acc ct = case isPendingScDict ct of
+                            Just ct' -> (ct':acc, ct')
+                            Nothing  -> (acc,     ct)
+       ; pending_given <- getPendingScDicts
+       ; if null pending_given && null pending_wanted
+         then return (True, wc)
+         else
+    do { new_given  <- makeSuperClasses pending_given
+       ; new_insols <- solveSimpleGivens new_given
+       ; new_wanted <-  makeSuperClasses pending_wanted
+       ; return (False, wc { wc_simple = unsolved' `unionBags` listToBag new_wanted
+                           , wc_insol = insols `unionBags` new_insols }) } }
 
 solveNestedImplications :: Bag Implication
                         -> TcS (Cts, Bag Implication)
@@ -1054,7 +1097,7 @@ solveImplication :: Implication    -- Wanted
 solveImplication imp@(Implic { ic_tclvl  = tclvl
                              , ic_binds  = m_ev_binds
                              , ic_skols  = skols
-                             , ic_given  = givens
+                             , ic_given  = given_ids
                              , ic_wanted = wanteds
                              , ic_info   = info
                              , ic_status = status
@@ -1071,15 +1114,21 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
 
          -- Solve the nested constraints
        ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs)
-             <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ givens)) tclvl $
-               do { given_insols <- solveSimpleGivens (mkGivenLoc tclvl info env) givens
-                  ; no_eqs <- getNoGivenEqs tclvl skols
+             <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $
+               do { let loc = mkGivenLoc tclvl info env
+                  ; givens_w_scs <- mkGivensWithSuperClasses loc given_ids
+                  ; given_insols <- solveSimpleGivens givens_w_scs
 
                   ; residual_wanted <- solveWanteds wanteds
                         -- solveWanteds, *not* solveWantedsAndDrop, because
                         -- we want to retain derived equalities so we can float
                         -- them out in floatEqualities
 
+                  ; no_eqs <- getNoGivenEqs tclvl skols
+                        -- Call getNoGivenEqs /after/ solveWanteds, because
+                        -- solveWanteds can augment the givens, via expandSuperClasses,
+                        -- to reveal given superclass equalities
+
                   ; return (no_eqs, given_insols, residual_wanted) }
 
        ; (floated_eqs, residual_wanted)
@@ -1355,27 +1404,17 @@ of progress.  Trac #8474 is a classic example:
 
   * So there is no point in attempting to re-solve
        ?yn:betan => [W] ?x:Int
-    because we'll just get the same [D] again
+    via solveNestedImplications, because we'll just get the
+    same [D] again
 
   * If we *do* re-solve, we'll get an ininite loop. It is cut off by
     the fixed bound of 10, but solving the next takes 10*10*...*10 (ie
     exponentially many) iterations!
 
-Conclusion: we should iterate simpl_loop iff we will get more 'givens'
-in the inert set when solving the nested implications.  That is the
-result of prepareInertsForImplications is larger.  How can we tell
-this?
-
-Consider floated_eqs (all wanted or derived):
-
-(a) [W/D] CTyEqCan (a ~ ty).  This can give rise to a new given only by causing
-    a unification. So we count those unifications.
-
-(b) [W] CFunEqCan (F tys ~ xi).  Even though these are wanted, they
-    are pushed in as givens by prepareInertsForImplications.  See Note
-    [Preparing inert set for implications] in TcSMonad.  But because
-    of that very fact, we won't generate another copy if we iterate
-    simpl_loop.  So we iterate if there any of these
+Conclusion: we should call solveNestedImplications only if we did
+some unifiction in solveSimpleWanteds; because that's the only way
+we'll get more Givens (a unificaiton is like adding a Given) to
+allow the implication to make progress.
 -}
 
 promoteTyVar :: TcLevel -> TcTyVar  -> TcM ()
index 915686b..7523c6a 100644 (file)
@@ -1927,9 +1927,6 @@ Validity checking is done once the mutually-recursive knot has been
 tied, so we can look at things freely.
 -}
 
-checkClassCycleErrs :: Class -> TcM ()
-checkClassCycleErrs cls = mapM_ recClsErr (calcClassCycles cls)
-
 checkValidTyCl :: TyCon -> TcM TyCon
 checkValidTyCl tc
   = setSrcSpan (getSrcSpan tc) $
@@ -2208,9 +2205,10 @@ checkNewDataCon con
 checkValidClass :: Class -> TcM ()
 checkValidClass cls
   = do  { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
-        ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
-        ; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
-        ; fundep_classes <- xoptM Opt_FunctionalDependencies
+        ; multi_param_type_classes  <- xoptM Opt_MultiParamTypeClasses
+        ; nullary_type_classes      <- xoptM Opt_NullaryTypeClasses
+        ; fundep_classes            <- xoptM Opt_FunctionalDependencies
+        ; undecidable_super_classes <- xoptM Opt_UndecidableSuperClasses
 
         -- Check that the class is unary, unless multiparameter type classes
         -- are enabled; also recognize deprecated nullary type classes
@@ -2225,7 +2223,11 @@ checkValidClass cls
 
           -- Now check for cyclic superclasses
           -- If there are superclass cycles, checkClassCycleErrs bails.
-        ; checkClassCycleErrs cls
+        ; unless undecidable_super_classes $
+          case checkClassCycles cls of
+             Just err -> setSrcSpan (getSrcSpan cls) $
+                         addErrTc err
+             Nothing  -> return ()
 
         -- Check the class operations.
         -- But only if there have been no earlier errors
@@ -2541,11 +2543,6 @@ recSynErr syn_decls
     sorted_decls = sortLocated syn_decls
     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
 
-recClsErr :: [TyCon] -> TcRn ()
-recClsErr cycles
-  = addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
-                 nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
-
 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
 badDataConTyCon data_con res_ty_tmpl actual_res_ty
   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
index 4798463..01ccae5 100644 (file)
@@ -13,7 +13,8 @@ files for imported data types.
 
 module TcTyDecls(
         calcRecFlags, RecTyInfo(..),
-        calcSynCycles, calcClassCycles,
+        calcSynCycles,
+        checkClassCycles,
 
         -- * Roles
         RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
@@ -56,19 +57,18 @@ import BasicTypes
 import SrcLoc
 import Unique ( mkBuiltinUnique )
 import Outputable
-import UniqSet
 import Util
 import Maybes
 import Data.List
 import Bag
-import FastString ( fastStringToByteString )
+import FastString
 
 import Control.Monad
 
 {-
 ************************************************************************
 *                                                                      *
-        Cycles in class and type synonym declarations
+        Cycles in type synonym declarations
 *                                                                      *
 ************************************************************************
 
@@ -139,123 +139,100 @@ mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
 calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
 calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
 
-{-
-Note [Superclass cycle check]
+{- Note [Superclass cycle check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We can't allow cycles via superclasses because it would result in the
-type checker looping when it canonicalises a class constraint (superclasses
-are added during canonicalisation).  More precisely, given a constraint
-    C ty1 .. tyn
-we want to instantiate all of C's superclasses, transitively, and
-that set must be finite.  So if
-     class (D b, E b a) => C a b
-then when we encounter the constraint
-     C ty1 ty2
-we'll instantiate the superclasses
-     (D ty2, E ty2 ty1)
-and then *their* superclasses, and so on.  This set must be finite!
-
-It is OK for superclasses to be type synonyms for other classes, so
-must "look through" type synonyms. Eg
-     type X a = C [a]
-     class X a => C a   -- No!  Recursive superclass!
-
-We want definitions such as:
-
-  class C cls a where cls a => a -> a
-  class C D a => D a where
-
-to be accepted, even though a naive acyclicity check would reject the
-program as having a cycle between D and its superclass.  Why? Because
-when we instantiate
-     D ty1
-we get the superclas
-     C D ty1
-and C has no superclasses, so we have terminated with a finite set.
-
-More precisely, the rule is this: the superclasses sup_C of a class C
-are rejected iff:
+The superclass cycle check for C decides if we can statically
+guarantee that expanding C's superclass cycles transitively is
+guaranteed to terminate.  This is a Haskell98 requirement,
+but one that we lift with -XUndecidableSuperClasses.
 
-  C \elem expand(sup_C)
-
-Where expand is defined as follows:
-
-(1)  expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-
-(2)  expand(D ty1 ... tyN) = {D}
-                             \union sup_D[ty1/x1, ..., tyP/xP]
-                             \union expand(ty(P+1)) ... \union expand(tyN)
-           where (D x1 ... xM) is a class, P = min(M,N)
-
-(3)  expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-        where T is not a class
-
-Eqn (1) is conservative; when there's a type variable at the head,
-look in all the argument types.  Eqn (2) expands superclasses; the
-third component of the union is like Eqn (1).  Eqn (3) happens mainly
-when the context is a (constraint) tuple, such as (Eq a, Show a).
-
-Furthermore, expand always looks through type synonyms.
+The worry is that a superclass cycle could make the type checker loop.
+More precisely, with a constraint (Given or Wanted)
+    C ty1 .. tyn
+one approach is to instantiate all of C's superclasses, transitively.
+We can only do so if that set is finite.
+
+This potential loop occurs only through superclasses.  This, for
+exmaple, is fine
+  class C a where
+    op :: C b => a -> b -> b
+even though C's full definition uses C.
+
+Making the check static also makes it conservative.  Eg
+  type family F a
+  class F a => C a
+Here an instance of (F a) might mention C:
+  type instance F [a] = C a
+and now we'd have a loop.
+
+The static check works like this, starting with C
+  * Look at C's superclass predicates
+  * If any is a type-function application,
+    or is headed by a type variable, fail
+  * If any has C at the head, fail
+  * If any has a type class D at the head,
+    make the same test with D
+
+A tricky point is: what if there is a type variable at the head?
+Consider this:
+   class f (C f) => C f
+   class c       => Id c
+and now expand superclasses for constraint (C Id):
+     C Id
+ --> Id (C Id)
+ --> C Id
+ --> ....
+Each step expands superclasses one layer, and clearly does not terminate.
 -}
 
-calcClassCycles :: Class -> [[TyCon]]
-calcClassCycles cls
-  = nubBy eqAsCycle $
-    expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
+checkClassCycles :: Class -> Maybe SDoc
+-- Nothing  <=> ok
+-- Just err <=> possible cycle error
+checkClassCycles cls
+  = do { (definite_cycle, err) <- go emptyNameSet cls
+       ; let herald | definite_cycle = ptext (sLit "Superclass cycle for")
+                    | otherwise      = ptext (sLit "Potential superclass cycle for")
+       ; return (vcat [ herald <+> quotes (ppr cls)
+                      , nest 2 err, hint]) }
   where
-    -- The last TyCon in the cycle is always the same as the first
-    eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
-    cycles xs = take n . map (take n) . tails . cycle $ xs
-      where n = length xs
-
-    -- No more superclasses to expand ==> no problems with cycles
-    -- See Note [Superclass cycle check]
-    expandTheta :: UniqSet Class -- Path of Classes to here in set form
-                -> [TyCon]       -- Path to here
-                -> ThetaType     -- Superclass work list
-                -> [[TyCon]]     -- Input error paths
-                -> [[TyCon]]     -- Final error paths
-    expandTheta _    _    []           = id
-    expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
-
-    expandType seen path (TyConApp tc tys)
-      -- Expand unsaturated classes to their superclass theta if they are yet unseen.
-      -- If they have already been seen then we have detected an error!
+    hint = ptext (sLit "Use UndecidableSuperClasses to accept this")
+
+    go :: NameSet -> Class -> Maybe (Bool, SDoc)
+    go so_far cls = firstJusts $
+                    map (go_pred (so_far `extendNameSet` getName cls)) $
+                    classSCTheta cls
+
+    go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc)
+       -- Nothing <=> ok
+       -- Just (True, err)  <=> definite cycle
+       -- Just (False, err) <=> possible cycle
+    go_pred so_far pred  -- NB: tcSplitTyConApp looks through synonyms
+       | Just (tc, _) <- tcSplitTyConApp_maybe pred
+       = go_tc so_far pred tc
+       | hasTyVarHead pred
+       = Just (False, hang (ptext (sLit "one of whose superclass constraints is headed by a type variable:"))
+                         2 (quotes (ppr pred)))
+       | otherwise
+       = Nothing
+
+    go_tc :: NameSet -> PredType -> TyCon -> Maybe (Bool, SDoc)
+    go_tc so_far pred tc
+      | isFamilyTyCon tc
+      = Just (False, hang (ptext (sLit "one of whose superclass constraints is headed by a type family:"))
+                        2 (quotes (ppr pred)))
       | Just cls <- tyConClass_maybe tc
-      , let (env, remainder) = papp (classTyVars cls) tys
-            rest_tys = either (const []) id remainder
-      = if cls `elementOfUniqSet` seen
-         then (reverse (classTyCon cls:path):)
-              . flip (foldr (expandType seen path)) tys
-         else expandTheta (addOneToUniqSet seen cls) (tc:path)
-                          (substTys (mkTopTCvSubst env) (classSCTheta cls))
-              . flip (foldr (expandType seen path)) rest_tys
-
-      -- For synonyms, try to expand them: some arguments might be
-      -- phantoms, after all. We can expand with impunity because at
-      -- this point the type synonym cycle check has already happened.
-      | Just (tvs, rhs) <- synTyConDefn_maybe tc
-      , let (env, remainder) = papp tvs tys
-            rest_tys = either (const []) id remainder
-      = expandType seen (tc:path) (substTy (mkTopTCvSubst env) rhs)
-        . flip (foldr (expandType seen path)) rest_tys
-
-      -- For non-class, non-synonyms, just check the arguments
-      | otherwise
-      = flip (foldr (expandType seen path)) tys
-
-    expandType _    _    (TyVarTy {})     = id
-    expandType _    _    (LitTy {})       = id
-    expandType seen path (AppTy t1 t2)    = expandType seen path t1 . expandType seen path t2
-    expandType seen path (ForAllTy b t)   = expandType seen path (binderType b) . expandType seen path t
-    expandType seen path (CastTy ty _co)  = expandType seen path ty
-    expandType _    _    (CoercionTy {})  = id
-
-    papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
-    papp []       tys      = ([], Right tys)
-    papp tvs      []       = ([], Left tvs)
-    papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
-      where (env, remainder) = papp tvs tys
+      = go_cls so_far cls
+      | otherwise   -- Equality predicate, for example
+      = Nothing
+
+    go_cls :: NameSet -> Class -> Maybe (Bool, SDoc)
+    go_cls so_far cls
+       | getName cls  `elemNameSet` so_far
+       = Just (True, ptext (sLit "one of whose superclasses is") <+> quotes (ppr cls))
+       | otherwise
+       = do { (b,err) <- go so_far cls
+          ; return (b, ptext (sLit "one of whose superclasses is") <+> quotes (ppr cls)
+                       $$ err) }
 
 {-
 ************************************************************************
index 69ac6b7..6b148cf 100644 (file)
@@ -88,7 +88,7 @@ module TcType (
 
   ---------------------------------
   -- Predicate types
-  mkMinimalBySCs, transSuperClasses, transSuperClassesPred,
+  mkMinimalBySCs, transSuperClasses,
   pickQuantifiablePreds,
   immSuperClasses,
   isImprovementPred,
@@ -1590,7 +1590,33 @@ canUnifyWithPolyType dflags details
       _other                         -> True
           -- We can have non-meta tyvars in given constraints
 
-{-
+{- Note [Expanding superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we expand superclasses, we use the following algorithm:
+
+expand( so_far, pred ) returns the transitive superclasses of pred,
+                               not including pred itself
+ 1. If pred is not a class constraint, return empty set
+       Otherwise pred = C ts
+ 2. If C is in so_far, return empty set (breaks loops)
+ 3. Find the immediate superclasses constraints of (C ts)
+ 4. For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )
+
+Notice that
+
+ * With normal Haskell-98 classes, the loop-detector will never bite,
+   so we'll get all the superclasses.
+
+ * Since there is only a finite number of distinct classes, expansion
+   must terminate.
+
+ * The loop breaking is a bit conservative. Notably, a tuple class
+   could contain many times without threatening termination:
+      (Eq a, (Ord a, Ix a))
+   And this is try of any class that we can statically guarantee
+   as non-recursive (in some sense).  For now, we just make a special
+   case for tuples
+
 ************************************************************************
 *                                                                      *
 \subsection{Predicate types}
@@ -1693,30 +1719,48 @@ pickQuantifiablePreds qtvs theta
 
 -- Superclasses
 
+type PredWithSCs = (PredType, [PredType])
+
 mkMinimalBySCs :: [PredType] -> [PredType]
 -- Remove predicates that can be deduced from others by superclasses
-mkMinimalBySCs ptys = [ pty | pty <- ptys
-                            , pty `not_in_preds` rec_scs ]
+-- Result is a subset of the input
+mkMinimalBySCs ptys = go preds_with_scs []
  where
-   rec_scs           = concatMap trans_super_classes ptys
-   not_in_preds p ps = not (any (eqType p) ps)
-
-   trans_super_classes pred   -- Superclasses of pred, excluding pred itself
-     = case classifyPredType pred of
-         ClassPred cls tys -> transSuperClasses cls tys
-         _                 -> []
-
-transSuperClasses :: Class -> [Type] -> [PredType]
-transSuperClasses cls tys    -- Superclasses of (cls tys),
-                             -- excluding (cls tys) itself
-  = concatMap transSuperClassesPred (immSuperClasses cls tys)
-
-transSuperClassesPred :: PredType -> [PredType]
--- (transSuperClassesPred p) returns (p : p's superclasses)
-transSuperClassesPred p
-  = case classifyPredType p of
-      ClassPred cls tys -> p : transSuperClasses cls tys
-      _                 -> [p]
+   preds_with_scs :: [PredWithSCs]
+   preds_with_scs = [ (pred, transSuperClasses pred)
+                    | pred <- ptys ]
+
+   go :: [PredWithSCs]   -- Work list
+      -> [PredWithSCs]   -- Accumulating result
+      -> [PredType]
+   go [] min_preds = map fst min_preds
+   go (work_item@(p,_) : work_list) min_preds
+     | p `in_cloud` work_list || p `in_cloud` min_preds
+     = go work_list min_preds
+     | otherwise
+     = go work_list (work_item : min_preds)
+
+   in_cloud :: PredType -> [PredWithSCs] -> Bool
+   in_cloud p ps = or [ p `eqType` p' | (_, scs) <- ps, p' <- scs ]
+
+transSuperClasses :: PredType -> [PredType]
+-- (transSuperClasses p) returns (p's superclasses)
+-- not including p
+-- See Note [Expanding superclasses]
+transSuperClasses p
+  = go emptyNameSet p
+  where
+    go :: NameSet -> PredType -> [PredType]
+    go rec_clss p
+       | ClassPred cls tys <- classifyPredType p
+       , let cls_nm = className cls
+       , not (cls_nm `elemNameSet` rec_clss)
+       , let rec_clss' | isCTupleClass cls = rec_clss
+                       | otherwise         = rec_clss `extendNameSet` cls_nm
+       = [ p' | sc <- immSuperClasses cls tys
+              , p'  <- sc : go rec_clss' sc ]
+       | otherwise
+       = []
 
 immSuperClasses :: Class -> [Type] -> [PredType]
 immSuperClasses cls tys
index d854650..09fddcc 100644 (file)
@@ -17,7 +17,7 @@ module Bag (
         filterBag, partitionBag, partitionBagWith,
         concatBag, catBagMaybes, foldBag, foldrBag, foldlBag,
         isEmptyBag, isSingletonBag, consBag, snocBag, anyBag,
-        listToBag, bagToList,
+        listToBag, bagToList, mapAccumBagL,
         foldrBagM, foldlBagM, mapBagM, mapBagM_,
         flatMapBagM, flatMapBagPairM,
         mapAndUnzipBagM, mapAccumBagLM,
@@ -30,7 +30,7 @@ import Util
 import MonadUtils
 import Control.Monad
 import Data.Data
-import Data.List ( partition )
+import Data.List ( partition, mapAccumL )
 import qualified Data.Foldable as Foldable
 
 infixr 3 `consBag`
@@ -265,6 +265,18 @@ mapAndUnzipBagM f (ListBag xs)    = do ts <- mapM f xs
                                        let (rs,ss) = unzip ts
                                        return (ListBag rs, ListBag ss)
 
+mapAccumBagL ::(acc -> x -> (acc, y)) -- ^ combining funcction
+            -> acc                    -- ^ initial state
+            -> Bag x                  -- ^ inputs
+            -> (acc, Bag y)           -- ^ final state, outputs
+mapAccumBagL _ s EmptyBag        = (s, EmptyBag)
+mapAccumBagL f s (UnitBag x)     = let (s1, x1) = f s x in (s1, UnitBag x1)
+mapAccumBagL f s (TwoBags b1 b2) = let (s1, b1') = mapAccumBagL f s  b1
+                                       (s2, b2') = mapAccumBagL f s1 b2
+                                   in (s2, TwoBags b1' b2')
+mapAccumBagL f s (ListBag xs)    = let (s', xs') = mapAccumL f s xs
+                                   in (s', ListBag xs')
+
 mapAccumBagLM :: Monad m
             => (acc -> x -> m (acc, y)) -- ^ combining funcction
             -> acc                      -- ^ initial state
index 566ecda..f9bd20d 100644 (file)
@@ -5996,6 +5996,55 @@ to subsume the ``OverloadedStrings`` extension (currently, as a special
 case, string literals benefit from statically allocated compact
 representation).
 
+Undecidable (or recursive) superclasses
+---------------------------------------
+
+The language extension ``-XUndecidableSuperClasses`` allows much more flexible
+constraints in superclasses.
+
+A class cannot generally have itself as a superclass. So this is illegal ::
+
+    class C a => D a where ...
+    class D a => C a where ...
+
+GHC implements this test conservatively when type functions, or type variables,
+are involved. For example ::
+
+    type family F a :: Constraint
+    class F a => C a where ...
+
+GHC will complain about this, because you might later add ::
+
+    type instance F Int = C Int
+
+and now we'd be in a superclass loop.  Here's an example involving a type variable ::
+
+   class f (C f) => C f
+   class c       => Id c
+
+If we expanded the superclasses of ``C Id`` we'd get first ``Id (C Id)`` and
+thence ``C Id`` again.
+
+But superclass constraints like these are sometimes useful, and the conservative
+check is annoying where no actual recursion is involved.
+
+Moreover genuninely-recursive superclasses are sometimes useful. Here's a real-life
+example (Trac #10318) ::
+
+     class (Frac (Frac a) ~ Frac a,
+            Fractional (Frac a),
+            IntegralDomain (Frac a))
+         => IntegralDomain a where
+      type Frac a :: *
+
+Here the superclass cycle does terminate but it's not entirely straightforward
+to see that it does.
+
+With the language extension ``-XUndecidableSuperClasses`` GHC lifts all restrictions
+on superclass constraints. If there really *is* a loop, GHC will only
+expand it to finite depth.
+
+
 .. _type-families:
 
 Type families
index d4c6697..0e74bef 100644 (file)
@@ -4,6 +4,8 @@
               MultiParamTypeClasses, FunctionalDependencies #-}
 {-# LANGUAGE AllowAmbiguousTypes #-}
   -- ip :: IP x a => a  is strictly speaking ambiguous, but IP is magic
+{-# LANGUAGE UndecidableSuperClasses #-}
+  -- Because of the type-variable superclasses for tuples
 
 {-# OPTIONS_GHC -fno-warn-unused-imports #-}
 -- -fno-warn-unused-imports needed for the GHC.Tuple import below. Sigh.
index a5fe638..6472310 100644 (file)
@@ -3,23 +3,23 @@ TYPE SIGNATURES
     forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
   test2 ::
     forall (f :: * -> *) b a.
-    (Num b, Num a, Applicative f) =>
+    (Applicative f, Num a, Num b) =>
     (a -> f b) -> f b
   test3 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test4 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test5 ::
     forall (m :: * -> *) a a1 a2.
-    (Monad m, Num a2) =>
+    (Num a2, Monad m) =>
     (a2 -> m a1) -> (a1 -> a1 -> m a) -> m a
   test6 ::
     forall r (m :: * -> *) a.
-    (Monad m, Num (m a)) =>
+    (Num (m a), Monad m) =>
     (m a -> m (m a)) -> r -> m a
 TYPE CONSTRUCTORS
 COERCION AXIOMS
index 1b4f8e6..b6d04ef 100644 (file)
@@ -34,6 +34,7 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
                              "AlternativeLayoutRule",
                              "AlternativeLayoutRuleTransitional",
                              "OverloadedLabels",
+                             "UndecidableSuperClasses",
                              "TemplateHaskellQuotes",
                              "MonadFailDesugaring",
                              "TypeInType"]
index 245881f..d5afe0a 100644 (file)
@@ -1 +1 @@
-f :: (Monad m, ?callStack::CallStack) => (m a, r) -> m b
+f :: (?callStack::CallStack, Monad m) => (m a, r) -> m b
diff --git a/testsuite/tests/indexed-types/should_compile/T10318.hs b/testsuite/tests/indexed-types/should_compile/T10318.hs
new file mode 100644 (file)
index 0000000..04a2ca1
--- /dev/null
@@ -0,0 +1,35 @@
+{-# LANGUAGE FlexibleContexts, TypeSynonymInstances,
+             FlexibleInstances, TypeFamilies,
+             UndecidableSuperClasses #-}
+
+module T10318 where
+
+-- | Product of non-zero elements always non-zero.
+-- Every integral domain has a field of fractions.
+-- The field of fractions of any field is itself.
+class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a))
+  => IntegralDomain a where
+  type Frac a :: *
+  embed :: a -> Frac a
+
+instance IntegralDomain Integer where
+  type Frac Integer = Rational
+  embed = fromInteger
+
+instance IntegralDomain Rational where
+  type Frac Rational = Rational
+  embed = id
+
+g :: IntegralDomain a => a -> a
+g x = g x
+
+h :: a -> Frac a
+h x = h x
+
+-- This is the test function
+
+f :: IntegralDomain a => a -> Frac a
+f x = g (h (h x))
+  -- Given: IntegralDomain (Frac a)
+  -- Wanted: IntegralDomain (Frac (Frac a))
+
diff --git a/testsuite/tests/indexed-types/should_compile/T11067.hs b/testsuite/tests/indexed-types/should_compile/T11067.hs
new file mode 100644 (file)
index 0000000..0074fae
--- /dev/null
@@ -0,0 +1,35 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T11067 where
+
+import Data.Monoid
+import GHC.Exts (Constraint)
+
+type family Skolem (p :: k -> Constraint) :: k
+type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1
+
+-- | A quantified constraint
+type Forall (p :: k -> Constraint) = p (Skolem p)
+type ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) = p (f (SkolemF p f))
+
+-- These work
+class ForallF Monoid t => Monoid1 t
+instance ForallF Monoid t => Monoid1 t
+
+class ForallF Monoid1 t => Monoid2 t
+instance ForallF Monoid1 t => Monoid2 t
+
+-- Changing f a ~ g a to, (Ord (f a), Ord (g a)), say, removes the error
+class (f a ~ g a) => H f g a
+instance (f a ~ g a) => H f g a
+
+-- This one gives a superclass cycle error.
+class Forall (H f g) => H1 f g
+instance Forall (H f g) => H1 f g
index 53d7942..1300626 100644 (file)
@@ -1,7 +1,7 @@
 TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   test2 ::
-    forall c t t1. (Num t, Num t1, Coll c, Elem c ~ (t, t1)) => c -> c
+    forall c t t1. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c open
index 0a0a491..c017701 100644 (file)
@@ -1,14 +1,4 @@
 
-T3208b.hs:15:10: error:
-    • Could not deduce: OTerm o0 ~ STerm o0 arising from a use of ‘fce’
-      from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
-        bound by the type signature for:
-                   fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-        at T3208b.hs:14:1-56
-      The type variable ‘o0’ is ambiguous
-    • In the expression: fce (apply f)
-      In an equation for ‘fce'’: fce' f = fce (apply f)
-
 T3208b.hs:15:15: error:
     • Could not deduce: OTerm o0 ~ STerm a
         arising from a use of ‘apply’
index 77e05d7..44cb453 100644 (file)
@@ -1,6 +1,6 @@
 
-T8889.hs:12:1: Warning:
+T8889.hs:12:1: warning:
     Top-level binding with no type signature:
       f :: forall (f :: * -> *) a b.
-           (C_fmap f a, C f) =>
+           (C f, C_fmap f a) =>
            (a -> b) -> f a -> f b
index 5de25bf..d4ff607 100644 (file)
@@ -266,3 +266,5 @@ test('T10806', normal, compile_fail, [''])
 test('T10815', normal, compile, [''])
 test('T10931', normal, compile, [''])
 test('T11187', normal, compile, [''])
+test('T11067', normal, compile, [''])
+test('T10318', normal, compile, [''])
index 459f6c8..e70a256 100644 (file)
@@ -1,13 +1,13 @@
 
 T1897b.hs:16:1: error:
-    Couldn't match type ‘Depend a’ with ‘Depend a0’
-    NB: ‘Depend’ is a type function, and may not be injective
-    The type variable ‘a0’ is ambiguous
-    Expected type: t (Depend a) -> Bool
-      Actual type: t (Depend a0) -> Bool
-    In the ambiguity check for the inferred type for ‘isValid’
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    When checking the inferred type
-      isValid :: forall a (t :: * -> *).
-                 (Foldable t, Bug a) =>
-                 t (Depend a) -> Bool
+    • Couldn't match type ‘Depend a’ with ‘Depend a0’
+      NB: ‘Depend’ is a type function, and may not be injective
+      The type variable ‘a0’ is ambiguous
+      Expected type: t (Depend a) -> Bool
+        Actual type: t (Depend a0) -> Bool
+    • In the ambiguity check for the inferred type for ‘isValid’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the inferred type
+        isValid :: forall a (t :: * -> *).
+                   (Bug a, Foldable t) =>
+                   t (Depend a) -> Bool
index ea3b1d4..f6a5dee 100644 (file)
@@ -1,23 +1,5 @@
 
 T3330a.hs:19:34: error:
-    • Couldn't match type ‘ix’
-                     with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’
-      ‘ix’ is a rigid type variable bound by
-        the type signature for:
-          children :: forall (s :: * -> *) ix (r :: * -> *).
-                      s ix -> PF s r ix -> [AnyF s]
-        at T3330a.hs:18:13
-      Expected type: (s0 ix0 -> ix1)
-                     -> r ix1 -> Writer [AnyF s] (r'0 ix1)
-      Actual type: s ix
-    • In the first argument of ‘hmapM’, namely ‘p’
-      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
-    • Relevant bindings include
-        x :: PF s r ix (bound at T3330a.hs:19:12)
-        p :: s ix (bound at T3330a.hs:19:10)
-        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)
-
-T3330a.hs:19:34: error:
     • Couldn't match type ‘s’ with ‘(->) (s0 ix0 -> ix1)’
       ‘s’ is a rigid type variable bound by
         the type signature for:
@@ -26,7 +8,7 @@ T3330a.hs:19:34: error:
         at T3330a.hs:18:13
       Expected type: (s0 ix0 -> ix1)
                      -> r ix1 -> Writer [AnyF s] (r'0 ix1)
-      Actual type: s ix
+        Actual type: s ix
     • In the first argument of ‘hmapM’, namely ‘p’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
     • Relevant bindings include
@@ -43,7 +25,7 @@ T3330a.hs:19:44: error:
                       s ix -> PF s r ix -> [AnyF s]
         at T3330a.hs:18:13
       Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))
-      Actual type: PF s r ix
+        Actual type: PF s r ix
     • In the third argument of ‘hmapM’, namely ‘x’
       In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
     • Relevant bindings include
index 60ae24c..2b0524f 100644 (file)
@@ -14,19 +14,3 @@ T4174.hs:42:12: error:
     • Relevant bindings include
         testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
           (bound at T4174.hs:42:1)
-
-T4174.hs:42:12: error:
-    • Couldn't match type ‘b’ with ‘RtsSpinLock’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          testcase :: forall (m :: * -> *) minor n t p a b.
-                      Monad m =>
-                      m (Field (Way (GHC6'8 minor) n t p) a b)
-        at T4174.hs:41:13
-      Expected type: m (Field (Way (GHC6'8 minor) n t p) a b)
-        Actual type: m (Field (WayOf m) SmStep RtsSpinLock)
-    • In the expression: sync_large_objects
-      In an equation for ‘testcase’: testcase = sync_large_objects
-    • Relevant bindings include
-        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
-          (bound at T4174.hs:42:1)
index d52f4b4..8ac3d94 100644 (file)
@@ -1,25 +1,12 @@
 
-T8227.hs:16:27:
-    Couldn't match expected type ‘Scalar (V a)’
-                with actual type ‘Scalar (V (Scalar (V a)))
-                                  -> Scalar (V (Scalar (V a)))’
-    In the expression: arcLengthToParam eps eps
-    In an equation for ‘absoluteToParam’:
-        absoluteToParam eps seg = arcLengthToParam eps eps
-    Relevant bindings include
-      seg :: a (bound at T8227.hs:16:21)
-      eps :: Scalar (V a) (bound at T8227.hs:16:17)
-      absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-        (bound at T8227.hs:16:1)
-
-T8227.hs:16:44:
-    Couldn't match expected type ‘Scalar (V (Scalar (V a)))’
-                with actual type ‘Scalar (V a)’
-    NB: ‘Scalar’ is a type function, and may not be injective
-    In the first argument of ‘arcLengthToParam’, namely ‘eps’
-    In the expression: arcLengthToParam eps eps
-    Relevant bindings include
-      seg :: a (bound at T8227.hs:16:21)
-      eps :: Scalar (V a) (bound at T8227.hs:16:17)
-      absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
-        (bound at T8227.hs:16:1)
+T8227.hs:16:44: error:
+    • Couldn't match expected type ‘Scalar (V (Scalar (V a)))’
+                  with actual type ‘Scalar (V a)’
+      NB: ‘Scalar’ is a type function, and may not be injective
+    • In the first argument of ‘arcLengthToParam’, namely ‘eps’
+      In the expression: arcLengthToParam eps eps
+    • Relevant bindings include
+        seg :: a (bound at T8227.hs:16:21)
+        eps :: Scalar (V a) (bound at T8227.hs:16:17)
+        absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
+          (bound at T8227.hs:16:1)
index 2d55f9d..36b0716 100644 (file)
@@ -1,77 +1,21 @@
 
-T9662.hs:49:7: error:
-    • Couldn't match type ‘k’ with ‘n
+T9662.hs:47:8: error:
+    • Couldn't match type ‘k’ with ‘Int
       ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
         at T9662.hs:44:9
-      ‘n’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
-      In the expression:
-        backpermute
-          (modify
-             (atom :. atom :. atom :. atom)
-             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-          id
-    • Relevant bindings include
-        test :: Shape (((sh :. k) :. m) :. n)
-                -> Shape (((sh :. m) :. n) :. k)
-          (bound at T9662.hs:45:1)
-
-T9662.hs:49:7: error:
-    • Couldn't match type ‘m’ with ‘k’
-      ‘m’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      ‘k’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
-      In the expression:
-        backpermute
-          (modify
-             (atom :. atom :. atom :. atom)
-             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-          id
-    • Relevant bindings include
-        test :: Shape (((sh :. k) :. m) :. n)
-                -> Shape (((sh :. m) :. n) :. k)
-          (bound at T9662.hs:45:1)
-
-T9662.hs:49:7: error:
-    • Couldn't match type ‘n’ with ‘m’
-      ‘n’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      ‘m’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. k) :. m) :. n)
-        Actual type: Exp (((sh :. k) :. m) :. n)
-                     -> Exp (((sh :. k) :. m) :. n)
-    • In the second argument of ‘backpermute’, namely ‘id’
+      Expected type: Exp (((sh :. k) :. m) :. n)
+                     -> Exp (((sh :. m) :. n) :. k)
+        Actual type: Exp
+                       (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
+                     -> Exp
+                          (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
+    • In the first argument of ‘backpermute’, namely
+        ‘(modify
+            (atom :. atom :. atom :. atom)
+            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
       In the expression:
         backpermute
           (modify
index cd977d1..bd4fcf4 100644 (file)
@@ -1,8 +1,14 @@
 
-mod40.hs:3:1:
-    Cycle in class declaration (via superclasses): C1 -> C2 -> C1
-    In the class declaration for ‘C1’
+mod40.hs:3:1: error:
+    • Superclass cycle for ‘C1’
+        one of whose superclasses is ‘C2’
+        one of whose superclasses is ‘C1’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C1’
 
-mod40.hs:4:1:
-    Cycle in class declaration (via superclasses): C2 -> C1 -> C2
-    In the class declaration for ‘C2’
+mod40.hs:4:1: error:
+    • Superclass cycle for ‘C2’
+        one of whose superclasses is ‘C1’
+        one of whose superclasses is ‘C2’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C2’
index 7554ce9..0f0d6f9 100644 (file)
@@ -1,8 +1,8 @@
 TYPE SIGNATURES
-  arbitCs1 :: forall a. (Enum a, Eq a, Show a) => a -> String
-  arbitCs2 :: forall a. (Show a, Enum a, Eq a) => a -> String
+  arbitCs1 :: forall a. (Show a, Eq a, Enum a) => a -> String
+  arbitCs2 :: forall a. (Show a, Eq a, Enum a) => a -> String
   arbitCs3 :: forall a. (Show a, Enum a, Eq a) => a -> String
-  arbitCs4 :: forall a. (Eq a, Enum a, Show a) => a -> String
+  arbitCs4 :: forall a. (Eq a, Show a, Enum a) => a -> String
   arbitCs5 :: forall a. (Eq a, Enum a, Show a) => a -> String
 TYPE CONSTRUCTORS
 COERCION AXIOMS
index 0c0410d..e7fc912 100644 (file)
@@ -21,8 +21,8 @@ TYPE SIGNATURES
   >> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
   >>= ::
     forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
-  ^ :: forall a b. (Integral b, Num a) => a -> b -> a
-  ^^ :: forall a b. (Fractional a, Integral b) => a -> b -> a
+  ^ :: forall a b. (Num a, Integral b) => a -> b -> a
+  ^^ :: forall a b. (Integral b, Fractional a) => a -> b -> a
   abs :: forall a. Num a => a -> a
   acos :: forall a. Floating a => a -> a
   acosh :: forall a. Floating a => a -> a
@@ -39,7 +39,7 @@ TYPE SIGNATURES
   atan2 :: forall a. RealFloat a => a -> a -> a
   atanh :: forall a. Floating a => a -> a
   break :: forall a. (a -> Bool) -> [a] -> ([a], [a])
-  ceiling :: forall a b. (Integral b, RealFrac a) => a -> b
+  ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
   compare :: forall a. Ord a => a -> a -> Ordering
   concat :: forall (t :: * -> *) a. Foldable t => t [a] -> [a]
   concatMap ::
@@ -56,7 +56,7 @@ TYPE SIGNATURES
   dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
   either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
   elem ::
-    forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
   encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
   enumFrom :: forall a. Enum a => a -> [a]
   enumFromThen :: forall a. Enum a => a -> a -> [a]
@@ -72,7 +72,7 @@ TYPE SIGNATURES
   floatDigits :: forall a. RealFloat a => a -> Int
   floatRadix :: forall a. RealFloat a => a -> Integer
   floatRange :: forall a. RealFloat a => a -> (Int, Int)
-  floor :: forall a b. (Integral b, RealFrac a) => a -> b
+  floor :: forall a b. (RealFrac a, Integral b) => a -> b
   fmap ::
     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
   foldl ::
@@ -89,7 +89,7 @@ TYPE SIGNATURES
     forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
   fromEnum :: forall a. Enum a => a -> Int
   fromInteger :: forall a. Num a => Integer -> a
-  fromIntegral :: forall a b. (Integral a, Num b) => a -> b
+  fromIntegral :: forall a b. (Num b, Integral a) => a -> b
   fromRational :: forall a. Fractional a => Rational -> a
   fst :: forall a b. (a, b) -> a
   gcd :: forall a. Integral a => a -> a -> a
@@ -118,24 +118,24 @@ TYPE SIGNATURES
   map :: forall a b. (a -> b) -> [a] -> [b]
   mapM ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, Traversable t) =>
+    (Traversable t, Monad m) =>
     (a -> m b) -> t a -> m (t b)
   mapM_ ::
     forall (t :: * -> *) (m :: * -> *) a b.
-    (Monad m, Foldable t) =>
+    (Foldable t, Monad m) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
   maxBound :: forall t. Bounded t => t
-  maximum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a
+  maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
   maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
   minBound :: forall t. Bounded t => t
-  minimum :: forall (t :: * -> *) a. (Ord a, Foldable t) => t a -> a
+  minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
   mod :: forall a. Integral a => a -> a -> a
   negate :: forall a. Num a => a -> a
   not :: Bool -> Bool
   notElem ::
-    forall (t :: * -> *) a. (Eq a, Foldable t) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
   null :: forall (t :: * -> *) a. Foldable t => t a -> Bool
   odd :: forall a. Integral a => a -> Bool
   or :: forall (t :: * -> *). Foldable t => t Bool -> Bool
@@ -143,9 +143,9 @@ TYPE SIGNATURES
   pi :: forall t. Floating t => t
   pred :: forall a. Enum a => a -> a
   print :: forall a. Show a => a -> IO ()
-  product :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a
+  product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
   properFraction ::
-    forall a b. (Integral b, RealFrac a) => a -> (b, a)
+    forall a b. (RealFrac a, Integral b) => a -> (b, a)
   putChar :: Char -> IO ()
   putStr :: String -> IO ()
   putStrLn :: String -> IO ()
@@ -159,14 +159,14 @@ TYPE SIGNATURES
   readParen :: forall a. Bool -> ReadS a -> ReadS a
   reads :: forall a. Read a => ReadS a
   readsPrec :: forall a. Read a => Int -> ReadS a
-  realToFrac :: forall a b. (Fractional b, Real a) => a -> b
+  realToFrac :: forall a b. (Real a, Fractional b) => a -> b
   recip :: forall a. Fractional a => a -> a
   rem :: forall a. Integral a => a -> a -> a
   repeat :: forall a. a -> [a]
   replicate :: forall a. Int -> a -> [a]
   return :: forall (m :: * -> *) a. Monad m => a -> m a
   reverse :: forall a. [a] -> [a]
-  round :: forall a b. (Integral b, RealFrac a) => a -> b
+  round :: forall a b. (RealFrac a, Integral b) => a -> b
   scaleFloat :: forall a. RealFloat a => Int -> a -> a
   scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
   scanl1 :: forall a. (a -> a -> a) -> [a] -> [a]
@@ -175,11 +175,11 @@ TYPE SIGNATURES
   seq :: forall a b. a -> b -> b
   sequence ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, Traversable t) =>
+    (Traversable t, Monad m) =>
     t (m a) -> m (t a)
   sequence_ ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (Monad m, Foldable t) =>
+    (Foldable t, Monad m) =>
     t (m a) -> m ()
   show :: forall a. Show a => a -> String
   showChar :: Char -> ShowS
@@ -198,7 +198,7 @@ TYPE SIGNATURES
   sqrt :: forall a. Floating a => a -> a
   subtract :: forall a. Num a => a -> a -> a
   succ :: forall a. Enum a => a -> a
-  sum :: forall (t :: * -> *) a. (Num a, Foldable t) => t a -> a
+  sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
   tail :: forall a. [a] -> [a]
   take :: forall a. Int -> [a] -> [a]
   takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
@@ -207,7 +207,7 @@ TYPE SIGNATURES
   toEnum :: forall a. Enum a => Int -> a
   toInteger :: forall a. Integral a => a -> Integer
   toRational :: forall a. Real a => a -> Rational
-  truncate :: forall a b. (Integral b, RealFrac a) => a -> b
+  truncate :: forall a b. (RealFrac a, Integral b) => a -> b
   uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
   undefined :: forall t. (?callStack::CallStack) => t
   unlines :: [String] -> String
index 8b9eb46..3fd0860 100644 (file)
@@ -10,7 +10,7 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
 WarningWildcardInstantiations.hs:5:14: warning:
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum a, Show a) => a -> String
+               the inferred type of foo :: (Show a, Enum a) => a -> String
                at WarningWildcardInstantiations.hs:6:1
     • In the type signature:
         foo :: (Show _a, _) => _a -> _
index 2df1544..30efb8f 100644 (file)
@@ -2,7 +2,7 @@
 InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
     • Found type wildcard ‘_a’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
+               the inferred type of foo :: (Show b, Enum b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:4:8
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
index 4085291..3244db6 100644 (file)
@@ -1,7 +1,7 @@
 
 T10999.hs:5:6: error:
-    Found constraint wildcard ‘_’ standing for ‘(Ord a,
-                                                 ?callStack::CallStack)’
+    Found constraint wildcard ‘_’ standing for ‘(?callStack::CallStack,
+                                                 Ord a)’
     To use the inferred type, enable PartialTypeSignatures
     In the type signature:
       f :: _ => () -> _
@@ -10,7 +10,7 @@ T10999.hs:5:17: error:
     • Found type wildcard ‘_’ standing for ‘Set.Set a’
       Where: ‘a’ is a rigid type variable bound by
                the inferred type of
-               f :: (Ord a, ?callStack::CallStack) => () -> Set.Set a
+               f :: (?callStack::CallStack, Ord a) => () -> Set.Set a
                at T10999.hs:6:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
index ddbb9e2..ff18935 100644 (file)
@@ -2,7 +2,7 @@
 WildcardInstantiations.hs:5:14: error:
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Enum a, Show a) => a -> String
+               the inferred type of foo :: (Show a, Enum a) => a -> String
                at WildcardInstantiations.hs:6:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
index 9b8785f..49a126b 100644 (file)
@@ -91,7 +91,7 @@ test('haddock.Cabal',
 test('haddock.compiler',
      [unless(in_tree_compiler(), skip), req_haddock
      ,stats_num_field('bytes allocated',
-          [(wordsize(64), 44721228752, 10)
+          [(wordsize(64), 49395782136, 10)
             # 2012P-08-14: 26070600504 (amd64/Linux)
             # 2012-08-29: 26353100288 (amd64/Linux, new CG)
             # 2012-09-18: 26882813032 (amd64/Linux)
@@ -103,6 +103,7 @@ test('haddock.compiler',
             # 2015-06-02: 36740649320 (amd64/Linux) unknown cause
             # 2015-06-29: 40624322224 (amd64/Linux) due to #10482, not yet investigated
             # 2015-12-03: 44721228752 (amd64/Linux) slow creep upwards
+            # 2015-12-15: 49395782136 (amd64/Linux) more creep, following kind-equalities
 
           ,(platform('i386-unknown-mingw32'),   902576468, 10)
             # 2012-10-30:                     13773051312 (x86/Windows)
index d2eb8cd..98e4cb9 100644 (file)
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-overlapping-patterns #-}
 
 module T3927b where
index 79623e9..a18b32b 100644 (file)
@@ -35,18 +35,36 @@ instance (Build dc r, a ~ dc) => Build dc (a->r) where
 tspan :: (Build (DC d) r, BuildR r ~ DC d) => r
 tspan = build (id :: DC d -> DC d) mempty
 
-{- Wanted:
+{- Solving 'tspan'
+
+Given:    Build (DC d) r, BuildR r ~ DC d
+ (by sc)  Monoid (DC d)
+
+   Wanted:
        Build acc0 r0
        Monid acc0
        acc0 ~ DC d0
        DC d0 ~ BuildR r0
+       r ~ r0
 ==>
-       Build (DC d0) r0
+       Build (DC d0) r
        Monoid (DC d0)  -->  Monoid d0
-       DC d- ~ BuildR r0
-
-In fact Monoid (DC d0) is a superclass of (Build (DC do) r0)
-But during inference we do not take upserclasses of wanteds
+       DC d0 ~ BuildR r
+
+From Given: BuildR r = DC d, hence
+       DC d0 ~ DC d
+hence
+       d0 ~ d
+
+===>
+       Build (DC d) r
+       Monoid (DC d)
+
+Now things are delicate.  Either the instance Monoid (DC d) will fire or,
+if we are lucky, we might spot that (Monoid (DC d)) is a superclass of
+a given.  But now (Decl 15) we add superclasses lazily, so that is less
+likely to happen, and was always fragile.  So include (MOnoid d) in the
+signature, as was the case in the orignal ticket.
 -}
 
 
index 18da703..ae21956 100644 (file)
@@ -1,11 +1,13 @@
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE UndecidableInstances  #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 {-# LANGUAGE KindSignatures        #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs           #-}
 {-# LANGUAGE Rank2Types      #-}
+
 module T7594 where
 
 import GHC.Exts (Constraint)
index 3ee902a..2f1844e 100644 (file)
@@ -1,15 +1,16 @@
 
-T7594.hs:33:12:
-    Couldn't match type ‘b’ with ‘IO ()’
-      ‘b’ is untouchable
-        inside the constraints: (:&:) c0 Real a
-        bound by a type expected by the context: (:&:) c0 Real a => a -> b
-        at T7594.hs:33:8-19
+T7594.hs:35:12: error:
+    • Couldn't match type ‘b’ with ‘IO ()’
+        ‘b’ is untouchable
+          inside the constraints: (:&:) c0 Real a
+          bound by a type expected by the context:
+                     (:&:) c0 Real a => a -> b
+          at T7594.hs:35:8-19
       ‘b’ is a rigid type variable bound by
-          the inferred type of bar2 :: b at T7594.hs:33:1
-    Possible fix: add a type signature for ‘bar2’
-    Expected type: a -> b
-      Actual type: a -> IO ()
-    In the first argument of ‘app’, namely ‘print’
-    In the expression: app print q2
-    Relevant bindings include bar2 :: b (bound at T7594.hs:33:1)
+        the inferred type of bar2 :: b at T7594.hs:35:1
+      Possible fix: add a type signature for ‘bar2’
+      Expected type: a -> b
+        Actual type: a -> IO ()
+    • In the first argument of ‘app’, namely ‘print’
+      In the expression: app print q2
+    • Relevant bindings include bar2 :: b (bound at T7594.hs:35:1)
index 857d11a..4a2473a 100644 (file)
@@ -11,16 +11,3 @@ T9017.hs:8:7: error:
       In an equation for ‘foo’: foo = arr return
     • Relevant bindings include
         foo :: a b (m b) (bound at T9017.hs:8:1)
-
-T9017.hs:8:7: error:
-    • Couldn't match kind ‘k1’ with ‘*’
-      ‘k1’ is a rigid type variable bound by
-        the type signature for:
-          foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k).
-                 a b (m b)
-        at T9017.hs:7:8
-      When matching the kind of ‘a’
-    • In the expression: arr return
-      In an equation for ‘foo’: foo = arr return
-    • Relevant bindings include
-        foo :: a b (m b) (bound at T9017.hs:8:1)
index e2411e1..296e691 100644 (file)
@@ -1,5 +1,5 @@
 
-T4398.hs:6:11: Warning:
+T4398.hs:6:11: warning:
     Forall'd constraint ‘Ord a’ is not bound in RULE lhs
       Orig bndrs: [a, $dOrd, x, y]
       Orig lhs: let {
index b88803c..031be76 100644 (file)
@@ -2,6 +2,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10100 where
 
index a61b2bc..a517eea 100644 (file)
@@ -1,5 +1,6 @@
 {-# LANGUAGE PolyKinds, MultiParamTypeClasses, FunctionalDependencies,
              UndecidableInstances, FlexibleInstances #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10109 where
 
index 7b19f00..4579dbe 100644 (file)
@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
              DataKinds, TypeFamilies, KindSignatures, PolyKinds, FunctionalDependencies #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 
 module T10564 where
 
index b3a6240..6232a4b 100644 (file)
@@ -1,41 +1,16 @@
 
 T9834.hs:23:10: warning:
-    • Couldn't match type ‘a’ with ‘p a0’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          afix :: forall a.
-                  (forall (q :: * -> *). Applicative q => Comp p q a -> Comp p q a)
-                  -> p a
-        at T9834.hs:22:11
-         Expected type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Comp p q a -> Comp p q a)
-                        -> p a
-           Actual type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Nat (Comp p q) (Comp p q))
-                        -> p a0 -> p a0
-    • In the expression: wrapIdComp
-      In an equation for ‘afix’: afix = wrapIdComp
-    • Relevant bindings include
-        afix :: (forall (q :: * -> *).
-                 Applicative q =>
-                 Comp p q a -> Comp p q a)
-                -> p a
-          (bound at T9834.hs:23:3)
-
-T9834.hs:23:10: warning:
     • Couldn't match type ‘p’ with ‘(->) (p a0)’
       ‘p’ is a rigid type variable bound by
         the class declaration for ‘ApplicativeFix’ at T9834.hs:21:39
-         Expected type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Comp p q a -> Comp p q a)
-                        -> p a
-           Actual type: (forall (q :: * -> *).
-                         Applicative q =>
-                         Nat (Comp p q) (Comp p q))
-                        -> p a0 -> p a0
+      Expected type: (forall (q :: * -> *).
+                      Applicative q =>
+                      Comp p q a -> Comp p q a)
+                     -> p a
+        Actual type: (forall (q :: * -> *).
+                      Applicative q =>
+                      Nat (Comp p q) (Comp p q))
+                     -> p a0 -> p a0
     • In the expression: wrapIdComp
       In an equation for ‘afix’: afix = wrapIdComp
     • Relevant bindings include
@@ -59,8 +34,8 @@ T9834.hs:23:10: warning:
           Applicative q =>
           Comp p q a1 -> Comp p q a1
         at T9834.hs:23:10
-         Expected type: Comp p q a1 -> Comp p q a1
-           Actual type: Comp p q a -> Comp p q a
+      Expected type: Comp p q a1 -> Comp p q a1
+        Actual type: Comp p q a -> Comp p q a
     • In the expression: wrapIdComp
       In an equation for ‘afix’: afix = wrapIdComp
     • Relevant bindings include
index d33f7a6..15c096e 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances, UndecidableSuperClasses #-}
 module Ctx where
 
 import Data.Kind ( Constraint )
index 0991dde..bba821b 100644 (file)
@@ -1,26 +1,13 @@
-\r
-T2714.hs:8:5: error:\r
-    Couldn't match type ‘a’ with ‘f0 b’\r
-    ‘a’ is a rigid type variable bound by\r
-    the type signature for:\r
-      f :: forall a b. ((a -> b) -> b) -> forall c. c -> a\r
-    at T2714.hs:7:6\r
-    Expected type: ((a -> b) -> b) -> c -> a\r
-      Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b\r
-    In the expression: ffmap\r
-    In an equation for ‘f’: f = ffmap\r
-    Relevant bindings include\r
-      f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)\r
-\r
-T2714.hs:8:5: error:\r
-    Couldn't match type ‘c’ with ‘f0 (a -> b)’\r
-    ‘c’ is a rigid type variable bound by\r
-    the type signature for:\r
-      f :: forall c. ((a -> b) -> b) -> c -> a\r
-    at T2714.hs:8:1\r
-    Expected type: ((a -> b) -> b) -> c -> a\r
-      Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b\r
-    In the expression: ffmap\r
-    In an equation for ‘f’: f = ffmap\r
-    Relevant bindings include\r
-      f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)\r
+
+T2714.hs:8:5: error:
+    • Couldn't match type ‘a’ with ‘f0 b’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. ((a -> b) -> b) -> forall c. c -> a
+        at T2714.hs:7:6
+      Expected type: ((a -> b) -> b) -> c -> a
+        Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b
+    • In the expression: ffmap
+      In an equation for ‘f’: f = ffmap
+    • Relevant bindings include
+        f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)
index dc23d4a..33ae4e1 100644 (file)
@@ -1,23 +1,23 @@
 
 T5853.hs:15:52: error:
-    • Could not deduce: Subst t1 (Elem t2) ~ t2
+    • Could not deduce: Subst t2 (Elem t1) ~ t1
         arising from a use of ‘<$>’
       from the context: (F t,
                          Elem t ~ Elem t,
-                         Elem t2 ~ Elem t2,
-                         Subst t (Elem t2) ~ t2,
-                         Subst t2 (Elem t) ~ t,
-                         F t1,
                          Elem t1 ~ Elem t1,
-                         Elem t ~ Elem t,
+                         Subst t (Elem t1) ~ t1,
                          Subst t1 (Elem t) ~ t,
-                         Subst t (Elem t1) ~ t1)
+                         F t2,
+                         Elem t2 ~ Elem t2,
+                         Elem t ~ Elem t,
+                         Subst t2 (Elem t) ~ t,
+                         Subst t (Elem t2) ~ t2)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      ‘t2’ is a rigid type variable bound by
+      ‘t1’ is a rigid type variable bound by
         the RULE "map/map" at T5853.hs:15:2
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t -> Elem t2 (bound at T5853.hs:15:19)
-        g :: Elem t1 -> Elem t (bound at T5853.hs:15:21)
-        xs :: t1 (bound at T5853.hs:15:23)
+        f :: Elem t -> Elem t1 (bound at T5853.hs:15:19)
+        g :: Elem t2 -> Elem t (bound at T5853.hs:15:21)
+        xs :: t2 (bound at T5853.hs:15:23)
index 6431c27..f906a95 100644 (file)
@@ -1,29 +1,16 @@
 
-T7869.hs:3:12:
-    Couldn't match type ‘a’ with ‘a1’
-      because type variable ‘a1’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      an expression type signature: [a1] -> b1
-      at T7869.hs:3:5-27
-    Expected type: [a1] -> b1
-      Actual type: [a] -> b
-    In the expression: f x
-    In the expression: (\ x -> f x) :: [a] -> b
-    In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    Relevant bindings include
-      x :: [a1] (bound at T7869.hs:3:7)
-      f :: [a] -> b (bound at T7869.hs:3:1)
-
-T7869.hs:3:12:
-    Couldn't match type ‘b’ with ‘b1’
-      because type variable ‘b1’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      an expression type signature: [a1] -> b1
-      at T7869.hs:3:5-27
-    Expected type: [a1] -> b1
-      Actual type: [a] -> b
-    In the expression: f x
-    In the expression: (\ x -> f x) :: [a] -> b
-    In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
-
+T7869.hs:3:12: error:
+    • Couldn't match type ‘a’ with ‘a1’
+        because type variable ‘a1’ would escape its scope
+      This (rigid, skolem) type variable is bound by
+        an expression type signature:
+          [a1] -> b1
+        at T7869.hs:3:5-27
+      Expected type: [a1] -> b1
+        Actual type: [a] -> b
+    • In the expression: f x
+      In the expression: (\ x -> f x) :: [a] -> b
+      In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)
index b18a97a..25fd7c0 100644 (file)
@@ -1,8 +1,8 @@
-\r
-T8883.hs:20:1: error:\r
-    Non type-variable argument in the constraint: Functor (PF a)\r
-    (Use FlexibleContexts to permit this)\r
-    When checking the inferred type\r
-      fold :: forall b a.\r
-              (Functor (PF a), Regular a) =>\r
-              (PF a b -> b) -> a -> b\r
+
+T8883.hs:20:1: error:
+    • Non type-variable argument in the constraint: Functor (PF a)
+      (Use FlexibleContexts to permit this)
+    • When checking the inferred type
+        fold :: forall b a.
+                (Regular a, Functor (PF a)) =>
+                (PF a b -> b) -> a -> b
index 516759e..3250b67 100644 (file)
@@ -1,8 +1,14 @@
 
-T9415.hs:3:1:
-    Cycle in class declaration (via superclasses): C -> D -> C
-    In the class declaration for ‘C’
+T9415.hs:3:1: error:
+    • Superclass cycle for ‘C’
+        one of whose superclasses is ‘D’
+        one of whose superclasses is ‘C’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C’
 
-T9415.hs:5:1:
-    Cycle in class declaration (via superclasses): D -> C -> D
-    In the class declaration for ‘D’
+T9415.hs:5:1: error:
+    • Superclass cycle for ‘D’
+        one of whose superclasses is ‘C’
+        one of whose superclasses is ‘D’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘D’
index 34e2f11..c35440a 100644 (file)
@@ -1,10 +1,14 @@
 
-T9739.hs:4:1:
-    Cycle in class declaration (via superclasses):
-      Class1 -> Class3 -> Class1
-    In the class declaration for ‘Class1’
+T9739.hs:4:1: error:
+    • Superclass cycle for ‘Class1’
+        one of whose superclasses is ‘Class3’
+        one of whose superclasses is ‘Class1’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘Class1’
 
-T9739.hs:9:1:
-    Cycle in class declaration (via superclasses):
-      Class3 -> Class1 -> Class3
-    In the class declaration for ‘Class3’
+T9739.hs:9:1: error:
+    • Superclass cycle for ‘Class3’
+        one of whose superclasses is ‘Class1’
+        one of whose superclasses is ‘Class3’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘Class3’
index 9cfdcf4..e8b2770 100644 (file)
@@ -1,8 +1,14 @@
 
-tcfail027.hs:4:1:
-    Cycle in class declaration (via superclasses): A -> B -> A
-    In the class declaration for ‘A’
+tcfail027.hs:4:1: error:
+    • Superclass cycle for ‘A’
+        one of whose superclasses is ‘B’
+        one of whose superclasses is ‘A’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’
 
-tcfail027.hs:7:1:
-    Cycle in class declaration (via superclasses): B -> A -> B
-    In the class declaration for ‘B’
+tcfail027.hs:7:1: error:
+    • Superclass cycle for ‘B’
+        one of whose superclasses is ‘A’
+        one of whose superclasses is ‘B’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘B’
index 34d4882..16a56e0 100644 (file)
@@ -1,4 +1,3 @@
--- Test we do get a cycle for superclasses escaping via a free tyvar
 {-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, UndecidableInstances #-}
 module TcFail where
 
index d354867..520f559 100644 (file)
@@ -1,4 +1,7 @@
 
-tcfail216.hs:5:1:
-    Cycle in class declaration (via superclasses): A -> A
-    In the class declaration for ‘A’
+tcfail216.hs:4:1: error:
+    • Potential superclass cycle for ‘A’
+        one of whose superclass constraints is headed by a type variable:
+          ‘cls (A cls)’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’
index 47c5078..62a6e5b 100644 (file)
@@ -4,4 +4,4 @@ module TcFail where
 
 type Aish = A
 
-class cls (Aish cls) => A cls c where
+class Aish a => A a where
index 0dc1a59..7290803 100644 (file)
@@ -1,4 +1,6 @@
 
 tcfail217.hs:7:1: error:
-    Cycle in class declaration (via superclasses): A -> Aish -> A
-    In the class declaration for ‘A’
+    • Superclass cycle for ‘A’
+        one of whose superclasses is ‘A’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘A’