Refactor tuple constraints

Make tuple constraints be handled by a perfectly ordinary
type class, with the component constraints being the
superclasses:
    class (c1, c2) => (c2, c2)

This change was provoked by

  #10359  inability to re-use a given tuple
          constraint as a whole

  #9858   confusion between term tuples
          and constraint tuples

but it's generally a very nice simplification. We get rid of
 -  In Type, the TuplePred constructor of PredTree,
    and all the code that dealt with TuplePreds
 -  In TcEvidence, the constructors EvTupleMk, EvTupleSel

See Note [How tuples work] in TysWiredIn.

Of course, nothing is ever entirely simple. This one
proved quite fiddly.

- I did quite a bit of renaming, which makes this patch
  touch a lot of modules. In partiuclar tupleCon -> tupleDataCon.

- I made constraint tuples known-key rather than wired-in.
  This is different to boxed/unboxed tuples, but it proved
  awkward to have all the superclass selectors wired-in.
  Easier just to use the standard mechanims.

- While I was fiddling with known-key names, I split the TH Name
  definitions out of DsMeta into a new module THNames.  That meant
  that the known-key names can all be gathered in PrelInfo, without
  causing module loops.

- I found that the parser was parsing an import item like
      T( .. )
  as a *data constructor* T, and then using setRdrNameSpace to
  fix it.  Stupid!  So I changed the parser to parse a *type
  constructor* T, which means less use of setRdrNameSpace.

  I also improved setRdrNameSpace to behave better on Exact Names.
  Largely on priciple; I don't think it matters a lot.

- When compiling a data type declaration for a wired-in thing like
  tuples (,), or lists, we don't really need to look at the
  declaration.  We have the wired-in thing!  And not doing so avoids
  having to line up the uniques for data constructor workers etc.
  See Note [Declarations for wired-in things]

- I found that FunDeps.oclose wasn't taking superclasses into
  account; easily fixed.

- Some error message refactoring for invalid constraints in TcValidity

18 files changed, 177 insertions, 183 deletions

diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index 53ecb48cc7..3e07f6b07c 100644
--- a/compiler/typecheck/FunDeps.hs
+++ b/compiler/typecheck/FunDeps.hs
@@ -23,6 +23,7 @@ import Name
 import Var
 import Class
 import Type
+import TcType( immSuperClasses )
 import Unify
 import InstEnv
 import VarSet
@@ -445,32 +446,29 @@ oclose :: [PredType] -> TyVarSet -> TyVarSet
 -- See Note [The liberal coverage condition]
 oclose preds fixed_tvs
   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
-  | otherwise   = loop fixed_tvs
+  | otherwise   = transCloVarSet extend fixed_tvs
   where
-    loop fixed_tvs
-      | new_fixed_tvs `subVarSet` fixed_tvs = fixed_tvs
-      | otherwise                           = loop new_fixed_tvs
-      where new_fixed_tvs = foldl extend fixed_tvs tv_fds
-
-    extend fixed_tvs (ls,rs)
-        | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
-        | otherwise                = fixed_tvs
+    extend fixed_tvs = foldl add fixed_tvs tv_fds
+       where
+          add fixed_tvs (ls,rs)
+            | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
+            | otherwise                = fixed_tvs
 
     tv_fds  :: [(TyVarSet,TyVarSet)]
     tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
-              | (xs, ys) <- concatMap determined preds
-              ]
+              | (xs, ys) <- concatMap determined preds ]
 
     determined :: PredType -> [([Type],[Type])]
     determined pred
        = case classifyPredType pred of
-            ClassPred cls tys ->
-               do let (cls_tvs, cls_fds) = classTvsFds cls
-                  fd <- cls_fds
-                  return (instFD fd cls_tvs tys)
             EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-            TuplePred ts       -> concatMap determined ts
-            _                  -> []
+            ClassPred cls tys -> local_fds ++ concatMap determined superclasses
+              where
+               local_fds = [ instFD fd cls_tvs tys
+                           | fd <- cls_fds ]
+               (cls_tvs, cls_fds) = classTvsFds cls
+               superclasses = immSuperClasses cls tys
+            _ -> []
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 78a53fba39..1383bdd909 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -173,42 +173,11 @@ canEvNC ev
                                   canClassNC ev cls tys
       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
                                   canEqNC    ev eq_rel ty1 ty2
-      TuplePred tys         -> do traceTcS "canEvNC:tup" (ppr tys)
-                                  canTuple   ev tys
       IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
                                   canIrred   ev
 {-
 ************************************************************************
 *                                                                      *
-*                      Tuple Canonicalization
-*                                                                      *
-************************************************************************
--}
-
-canTuple :: CtEvidence -> [PredType] -> TcS (StopOrContinue Ct)
-canTuple ev preds
-  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
-  = do { new_evars <- mapM (newWantedEvVar loc) preds
-       ; setWantedEvBind evar (EvTupleMk (map (ctEvId . fst) new_evars))
-       ; emitWorkNC (freshGoals new_evars)
-         -- Note the "NC": these are fresh goals, not necessarily canonical
-       ; stopWith ev "Decomposed tuple constraint" }
-
-  | CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
-  = do { given_evs <- newGivenEvVars loc (mkEvTupleSelectors (EvId evar) preds)
-       ; emitWorkNC given_evs
-       ; stopWith ev "Decomposed tuple constraint" }
-
-  | CtDerived { ctev_loc = loc } <- ev
-  = do { mapM_ (emitNewDerived loc) preds
-       ; stopWith ev "Decomposed tuple constraint" }
-
-  | otherwise = panic "canTuple"
-
-
-{-
-************************************************************************
-*                                                                      *
 *                      Class Canonicalization
 *                                                                      *
 ************************************************************************
@@ -384,7 +353,6 @@ canIrred old_ev
     do { -- Re-classify, in case flattening has improved its shape
        ; case classifyPredType (ctEvPred new_ev) of
            ClassPred cls tys     -> canClassNC new_ev cls tys
-           TuplePred tys         -> canTuple   new_ev tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
                                     CIrredEvCan { cc_ev = new_ev } } }
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 88c88bdc53..a4c4703ec3 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -320,8 +320,6 @@ reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = impli
        ; (_, leftovers) <- tryReporters ctxt2' reporters (insols2 ++ tidy_simples)
        ; MASSERT2( null leftovers, ppr leftovers )
 
-            -- TuplePreds should have been expanded away by the constraint
-            -- simplifier, so they shouldn't show up at this point
             -- All the Derived ones have been filtered out of simples
             -- by the constraint solver. This is ok; we don't want
             -- to report unsolved Derived goals as errors
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 6dd01f9f1f..6e026941f8 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -14,7 +14,7 @@ module TcEvidence (
   EvBindMap(..), emptyEvBindMap, extendEvBinds,
                  lookupEvBind, evBindMapBinds, foldEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
-  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvTupleSelectors, mkEvScSelectors,
+  EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
   EvLit(..), evTermCoercion,
   EvCallStack(..),
   EvTypeable(..),
@@ -712,10 +712,6 @@ data EvTerm
   | EvDFunApp DFunId             -- Dictionary instance application
        [Type] [EvId]
 
-  | EvTupleSel EvTerm Int        -- n'th component of the tuple, 0-indexed
-
-  | EvTupleMk [EvId]             -- tuple built from this stuff
-
   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors
                                -- See Note [Deferring coercion errors to runtime]
                                -- in TcSimplify
@@ -975,11 +971,6 @@ mkEvCast ev lco
     isTcReflCo lco = ev
   | otherwise      = EvCast ev lco
 
-mkEvTupleSelectors :: EvTerm -> [TcPredType] -> [(TcPredType, EvTerm)]
-mkEvTupleSelectors ev preds = zipWith mk_pr preds [0..]
-  where
-    mk_pr pred i = (pred, EvTupleSel ev i)
-
 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
 mkEvScSelectors ev cls tys
    = zipWith mk_pr (immSuperClasses cls tys) [0..]
@@ -1006,10 +997,8 @@ evVarsOfTerm :: EvTerm -> VarSet
 evVarsOfTerm (EvId v)             = unitVarSet v
 evVarsOfTerm (EvCoercion co)      = coVarsOfTcCo co
 evVarsOfTerm (EvDFunApp _ _ evs)  = mkVarSet evs
-evVarsOfTerm (EvTupleSel ev _)    = evVarsOfTerm ev
 evVarsOfTerm (EvSuperClass v _)   = evVarsOfTerm v
 evVarsOfTerm (EvCast tm co)       = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
-evVarsOfTerm (EvTupleMk evs)      = mkVarSet evs
 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
 evVarsOfTerm (EvLit _)            = emptyVarSet
 evVarsOfTerm (EvCallStack cs)     = evVarsOfCallStack cs
@@ -1089,8 +1078,6 @@ instance Outputable EvTerm where
   ppr (EvId v)              = ppr v
   ppr (EvCast v co)         = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
   ppr (EvCoercion co)       = ptext (sLit "CO") <+> ppr co
-  ppr (EvTupleSel v n)      = ptext (sLit "tupsel") <> parens (ppr (v,n))
-  ppr (EvTupleMk vs)        = ptext (sLit "tupmk") <+> ppr vs
   ppr (EvSuperClass d n)    = ptext (sLit "sc") <> parens (ppr (d,n))
   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
   ppr (EvLit l)             = ppr l
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 155cdb42be..a9622588a0 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -16,7 +16,7 @@ module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC,
 #include "HsVersions.h"
 
 import {-# SOURCE #-}   TcSplice( tcSpliceExpr, tcTypedBracket, tcUntypedBracket )
-import DsMeta( liftStringName, liftName )
+import THNames( liftStringName, liftName )
 
 import HsSyn
 import TcHsSyn
@@ -373,7 +373,7 @@ tcExpr (SectionL arg1 op) res_ty
 
 tcExpr (ExplicitTuple tup_args boxity) res_ty
   | all tupArgPresent tup_args
-  = do { let tup_tc = tupleTyCon (boxityNormalTupleSort boxity) (length tup_args)
+  = do { let tup_tc = tupleTyCon boxity (length tup_args)
        ; (coi, arg_tys) <- matchExpectedTyConApp tup_tc res_ty
        ; tup_args1 <- tcTupArgs tup_args arg_tys
        ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
@@ -383,7 +383,7 @@ tcExpr (ExplicitTuple tup_args boxity) res_ty
     do { let kind = case boxity of { Boxed   -> liftedTypeKind
                                    ; Unboxed -> openTypeKind }
              arity = length tup_args
-             tup_tc = tupleTyCon (boxityNormalTupleSort boxity) arity
+             tup_tc = tupleTyCon boxity arity
 
        ; arg_tys <- newFlexiTyVarTys (tyConArity tup_tc) kind
        ; let actual_res_ty
@@ -1273,14 +1273,14 @@ checkCrossStageLifting id (Brack _ (TcPending ps_var lie_var))
                -- just going to flag an error for now
 
         ; lift <- if isStringTy id_ty then
-                     do { sid <- tcLookupId DsMeta.liftStringName
+                     do { sid <- tcLookupId THNames.liftStringName
                                      -- See Note [Lifting strings]
                         ; return (HsVar sid) }
                   else
                      setConstraintVar lie_var   $
                           -- Put the 'lift' constraint into the right LIE
                      newMethodFromName (OccurrenceOf (idName id))
-                                       DsMeta.liftName id_ty
+                                       THNames.liftName id_ty
 
                    -- Update the pending splices
         ; ps <- readMutVar ps_var
diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
index d18e6edb60..d30c1ca3b1 100644
--- a/compiler/typecheck/TcGenDeriv.hs
+++ b/compiler/typecheck/TcGenDeriv.hs
@@ -1608,7 +1608,7 @@ data FFoldType a      -- Describes how to fold over a Type in a functor like way
         , ft_var     :: a                   -- The variable itself
         , ft_co_var  :: a                   -- The variable itself, contravariantly
         , ft_fun     :: a -> a -> a         -- Function type
-        , ft_tup     :: TupleSort -> [a] -> a  -- Tuple type
+        , ft_tup     :: TyCon -> [a] -> a   -- Tuple type
         , ft_ty_app  :: Type -> a -> a      -- Type app, variable only in last argument
         , ft_bad_app :: a                   -- Type app, variable other than in last argument
         , ft_forall  :: TcTyVar -> a -> a   -- Forall type
@@ -1644,8 +1644,7 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial,     ft_var = caseVar
        | not (or xcs)     = (caseTrivial, False)   -- Variable does not occur
        -- At this point we know that xrs, xcs is not empty,
        -- and at least one xr is True
-       | Just sort <- tyConTuple_maybe con
-                          = (caseTuple sort xrs, True)
+       | isTupleTyCon con = (caseTuple con xrs, True)
        | or (init xcs)    = (caseWrongArg, True)         -- T (..var..)    ty
        | Just (fun_ty, _) <- splitAppTy_maybe ty         -- T (..no var..) ty
                           = (caseTyApp fun_ty (last xrs), True)
@@ -1716,11 +1715,11 @@ mkSimpleConMatch fold extra_pats con insides = do
 -- "case x of (a1,a2,a3) -> fold [x1 a1, x2 a2, x3 a3]"
 mkSimpleTupleCase :: Monad m => ([LPat RdrName] -> DataCon -> [a]
                                  -> m (LMatch RdrName (LHsExpr RdrName)))
-                  -> TupleSort -> [a] -> LHsExpr RdrName -> m (LHsExpr RdrName)
-mkSimpleTupleCase match_for_con sort insides x = do
-    let con = tupleCon sort (length insides)
-    match <- match_for_con [] con insides
-    return $ nlHsCase x [match]
+                  -> TyCon -> [a] -> LHsExpr RdrName -> m (LHsExpr RdrName)
+mkSimpleTupleCase match_for_con tc insides x
+  = do { let data_con = tyConSingleDataCon tc
+       ; match <- match_for_con [] data_con insides
+       ; return $ nlHsCase x [match] }
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 80dd175e3c..02d993f70c 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -90,7 +90,7 @@ hsPatType (ViewPat _ _ ty)            = ty
 hsPatType (ListPat _ ty Nothing)      = mkListTy ty
 hsPatType (ListPat _ _ (Just (ty,_))) = ty
 hsPatType (PArrPat _ ty)              = mkPArrTy ty
-hsPatType (TuplePat _ bx tys)         = mkTupleTy (boxityNormalTupleSort bx) tys
+hsPatType (TuplePat _ bx tys)         = mkTupleTy bx tys
 hsPatType (ConPatOut { pat_con = L _ con, pat_arg_tys = tys })
                                       = conLikeResTy con tys
 hsPatType (SigPatOut _ ty)            = ty
@@ -1247,7 +1247,6 @@ zonkEvTerm env (EvCoercion co)    = do { co' <- zonkTcCoToCo env co
 zonkEvTerm env (EvCast tm co)     = do { tm' <- zonkEvTerm env tm
                                        ; co' <- zonkTcCoToCo env co
                                        ; return (mkEvCast tm' co') }
-zonkEvTerm env (EvTupleMk tms)    = return (EvTupleMk (zonkIdOccs env tms))
 zonkEvTerm _   (EvLit l)          = return (EvLit l)
 
 zonkEvTerm env (EvTypeable ev) =
@@ -1271,8 +1270,6 @@ zonkEvTerm env (EvCallStack cs)
       EvCsPushCall n l tm -> do { tm' <- zonkEvTerm env tm
                                 ; return (EvCallStack (EvCsPushCall n l tm')) }
 
-zonkEvTerm env (EvTupleSel tm n)  = do { tm' <- zonkEvTerm env tm
-                                       ; return (EvTupleSel tm' n) }
 zonkEvTerm env (EvSuperClass d n) = do { d' <- zonkEvTerm env d
                                        ; return (EvSuperClass d' n) }
 zonkEvTerm env (EvDFunApp df tys tms)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index fbd21b23f1..785dce751e 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -476,8 +476,8 @@ tc_hs_type hs_ty@(HsExplicitListTy _k tys) exp_kind
 tc_hs_type hs_ty@(HsExplicitTupleTy _ tys) exp_kind
   = do { tks <- mapM tc_infer_lhs_type tys
        ; let n          = length tys
-             kind_con   = promotedTupleTyCon   BoxedTuple n
-             ty_con     = promotedTupleDataCon BoxedTuple n
+             kind_con   = promotedTupleTyCon   Boxed n
+             ty_con     = promotedTupleDataCon Boxed n
              (taus, ks) = unzip tks
              tup_k      = mkTyConApp kind_con ks
        ; checkExpectedKind hs_ty tup_k exp_kind
@@ -568,10 +568,15 @@ finish_tuple :: HsType Name -> TupleSort -> [TcType] -> ExpKind -> TcM TcType
 finish_tuple hs_ty tup_sort tau_tys exp_kind
   = do { traceTc "finish_tuple" (ppr res_kind $$ ppr exp_kind $$ ppr exp_kind)
        ; checkExpectedKind hs_ty res_kind exp_kind
-       ; checkWiredInTyCon tycon
+       ; tycon <- case tup_sort of
+           ConstraintTuple -> tcLookupTyCon (cTupleTyConName arity)
+           BoxedTuple      -> do { let tc = tupleTyCon Boxed arity
+                                 ; checkWiredInTyCon tc
+                                 ; return tc }
+           UnboxedTuple    -> return (tupleTyCon Unboxed arity)
        ; return (mkTyConApp tycon tau_tys) }
   where
-    tycon = tupleTyCon tup_sort (length tau_tys)
+    arity = length tau_tys
     res_kind = case tup_sort of
                  UnboxedTuple    -> unliftedTypeKind
                  BoxedTuple      -> liftedTypeKind
@@ -1558,7 +1563,7 @@ tc_hs_kind (HsTupleTy _ kis) =
      checkWiredInTyCon tycon
      return $ mkTyConApp tycon kappas
   where
-     tycon = promotedTupleTyCon BoxedTuple (length kis)
+     tycon = promotedTupleTyCon Boxed (length kis)
 
 -- Argument not kind-shaped
 tc_hs_kind k = pprPanic "tc_hs_kind" (ppr k)
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index ed4fd913bf..de5df6ae53 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -1015,7 +1015,6 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
     super_classes ev_pair
       = case classifyPredType pred of
           ClassPred cls tys -> (pred, ev_tm) : super_classes_help ev_tm cls tys
-          TuplePred preds   -> concatMap super_classes (mkEvTupleSelectors ev_tm preds)
           _                 -> []
       where
         (pred, ev_tm) = normalise_pr ev_pair
@@ -1023,7 +1022,8 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds fam_envs sc_th
     ------------
     super_classes_help :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
     super_classes_help ev_tm cls tys  -- ev_tm :: cls tys
-      | sizeTypes tys >= head_size  -- Here is where we test for
+      | not (isCTupleClass cls)
+      , sizeTypes tys >= head_size  -- Here is where we test for
       = []                          -- a smaller dictionary
       | otherwise
       = concatMap super_classes (mkEvScSelectors ev_tm cls tys)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 95715fe03d..ce51b0d796 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -27,6 +27,7 @@ import PrelNames ( knownNatClassName, knownSymbolClassName, ipClassNameKey,
 import Id( idType )
 import Class
 import TyCon
+import DataCon( dataConWrapId )
 import FunDeps
 import FamInst
 import Inst( tyVarsOfCt )
@@ -2022,8 +2023,15 @@ matchClassInst _ clas [ ty ] _
     = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
                      $$ vcat (map (ppr . idType) (classMethods clas)))
 
+matchClassInst _ clas ts _
+  | isCTupleClass clas
+  , let data_con = tyConSingleDataCon (classTyCon clas)
+  = return (GenInst ts (EvDFunApp (dataConWrapId data_con) ts))
+            -- The dfun is the data constructor!
+
 matchClassInst _ clas [k,t] _
-  | className clas == typeableClassName = matchTypeableClass clas k t
+  | className clas == typeableClassName
+  = matchTypeableClass clas k t
 
 matchClassInst inerts clas tys loc
    = do { dflags <- getDynFlags
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 0eaae8f54b..a5d55555bc 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -143,7 +143,6 @@ predTypeOccName :: PredType -> OccName
 predTypeOccName ty = case classifyPredType ty of
     ClassPred cls _ -> mkDictOcc (getOccName cls)
     EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
-    TuplePred _     -> mkVarOccFS (fsLit "tup")
     IrredPred _     -> mkVarOccFS (fsLit "irred")
 
 
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 93c4728e45..df2ad1837d 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -589,7 +589,7 @@ tc_pat penv (PArrPat pats _) pat_ty thing_inside
         }
 
 tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
-  = do  { let tc = tupleTyCon (boxityNormalTupleSort boxity) (length pats)
+  = do  { let tc = tupleTyCon boxity (length pats)
         ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) pat_ty
         ; (pats', res) <- tc_lpats penv pats arg_tys thing_inside
 
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index ea454d5d60..820e969cf4 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -1016,6 +1016,10 @@ checkTc :: Bool -> MsgDoc -> TcM ()         -- Check that the boolean is true
 checkTc True  _   = return ()
 checkTc False err = failWithTc err
 
+failIfTc :: Bool -> MsgDoc -> TcM ()         -- Check that the boolean is false
+failIfTc False _   = return ()
+failIfTc True  err = failWithTc err
+
 --         Warnings have no 'M' variant, nor failure
 
 warnTc :: Bool -> MsgDoc -> TcM ()
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index e9705790ed..ee0740f8e4 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -614,7 +614,6 @@ pickQuantifiablePreds qtvs theta
 
           EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
           IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs
-          TuplePred {}          -> False
 
     pick_cls_pred flex_ctxt tys
       = tyVarsOfTypes tys `intersectsVarSet` qtvs
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 4ecbd5053c..a7363d85a1 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -38,7 +38,7 @@ import Outputable
 import TcExpr
 import SrcLoc
 import FastString
-import DsMeta
+import THNames
 import TcUnify
 import TcEnv
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 6ac87206bd..59ff6cb79e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -581,13 +581,24 @@ Then:
 This fancy footwork (with two bindings for T) is only necesary for the
 TyCons or Classes of this recursive group.  Earlier, finished groups,
 live in the global env only.
+
+Note [Declarations for wired-in things]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For wired-in things we simply ignore the declaration
+and take the wired-in information.  That avoids complications.
+e.g. the need to make the data constructor worker name for
+     a constraint tuple match the wired-in one
 -}
 
 tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
 tcTyClDecl rec_info (L loc decl)
+  | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
+  = return [thing]  -- See Note [Declarations for wired-in things]
+
+  | otherwise
   = setSrcSpan loc $ tcAddDeclCtxt decl $
-    traceTc "tcTyAndCl-x" (ppr decl) >>
-    tcTyClDecl1 NoParentTyCon rec_info decl
+    do { traceTc "tcTyAndCl-x" (ppr decl)
+       ; tcTyClDecl1 NoParentTyCon rec_info decl }
 
   -- "type family" declarations
 tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
@@ -788,7 +799,7 @@ tcDataDefn rec_info tc_name tvs kind
                  else case new_or_data of
                    DataType -> return (mkDataTyConRhs data_cons)
                    NewType  -> ASSERT( not (null data_cons) )
-                                    mkNewTyConRhs tc_name tycon (head data_cons)
+                               mkNewTyConRhs tc_name tycon (head data_cons)
              ; return (buildAlgTyCon tc_name final_tvs roles (fmap unLoc cType)
                                      stupid_theta tc_rhs
                                      (rti_is_rec rec_info tc_name)
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4d4f6823f2..9ce14497b7 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1377,7 +1377,6 @@ mkMinimalBySCs ptys = [ ploc |  ploc <- ptys
    trans_super_classes pred   -- Superclasses of pred, excluding pred itself
      = case classifyPredType pred of
          ClassPred cls tys -> transSuperClasses cls tys
-         TuplePred ts      -> concatMap trans_super_classes ts
          _                 -> []
 
 transSuperClasses :: Class -> [Type] -> [PredType]
@@ -1387,10 +1386,9 @@ transSuperClasses cls tys    -- Superclasses of (cls tys),
 
 transSuperClassesPred :: PredType -> [PredType]
 -- (transSuperClassesPred p) returns (p : p's superclasses)
-transSuperClassesPred p 
+transSuperClassesPred p
   = case classifyPredType p of
       ClassPred cls tys -> p : transSuperClasses cls tys
-      TuplePred ps      -> concatMap transSuperClassesPred ps
       _                 -> [p]
 
 immSuperClasses :: Class -> [Type] -> [PredType]
@@ -1406,7 +1404,6 @@ isImprovementPred ty
       EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
       EqPred ReprEq _ _  -> False
       ClassPred cls _    -> classHasFds cls
-      TuplePred ts       -> any isImprovementPred ts
       IrredPred {}       -> True -- Might have equalities after reduction?
 
 {-
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 3225b2848b..16059e68b5 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -24,13 +24,13 @@ import TypeRep
 import TcType
 import TcMType
 import TysWiredIn ( coercibleClass, eqTyConName )
+import PrelNames
 import Type
 import Unify( tcMatchTyX )
 import Kind
 import CoAxiom
 import Class
 import TyCon
-import PrelNames( eqTyConKey )
 
 -- others:
 import HsSyn            -- HsType
@@ -45,7 +45,6 @@ import Util
 import ListSetOps
 import SrcLoc
 import Outputable
-import Unique           ( hasKey )
 import BasicTypes       ( IntWithInf, infinity )
 import FastString
 
@@ -396,7 +395,11 @@ check_type ctxt rank ty
   = do  { checkTc (forAllAllowed rank) (forAllTyErr rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
-        ; check_valid_theta ctxt theta
+
+        ; check_valid_theta SigmaCtxt theta
+                -- Allow     type T = ?x::Int => Int -> Int
+                -- but not   type T = ?x::Int
+
         ; check_type ctxt rank tau }      -- Allow foralls to right of arrow
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
@@ -617,15 +620,16 @@ check_pred_help :: Bool    -- True <=> under a type synonym
 check_pred_help under_syn dflags ctxt pred
   | Just pred' <- coreView pred  -- Switch on under_syn when going under a
                                  -- synonym (Trac #9838, yuk)
-  = check_pred_help True dflags ctxt pred'  
+  = check_pred_help True dflags ctxt pred'
   | otherwise
   = case splitTyConApp_maybe pred of
-      Just (tc, tys) | Just cls <- tyConClass_maybe tc
-                     -> check_class_pred dflags ctxt pred cls tys  -- Includes Coercible
-                     | tc `hasKey` eqTyConKey
-                     -> check_eq_pred dflags pred tys
-                     | isTupleTyCon tc
-                     -> check_tuple_pred under_syn dflags ctxt pred tys
+      Just (tc, tys)
+        | isTupleTyCon tc
+        -> check_tuple_pred under_syn dflags ctxt pred tys
+        | Just cls <- tyConClass_maybe tc
+        -> check_class_pred dflags ctxt pred cls tys  -- Includes Coercible
+        | tc `hasKey` eqTyConKey
+        -> check_eq_pred dflags pred tys
       _ -> check_irred_pred under_syn dflags ctxt pred
 
 check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
@@ -656,16 +660,22 @@ check_irred_pred under_syn dflags ctxt pred
          --   see Note [ConstraintKinds in predicates]
          -- But (X t1 t2) is always ok because we just require ConstraintKinds
          -- at the definition site (Trac #9838)
-        checkTc (under_syn || xopt Opt_ConstraintKinds dflags || not (hasTyVarHead pred))
-                (predIrredErr pred)
+        failIfTc (not under_syn && not (xopt Opt_ConstraintKinds dflags)
+                                && hasTyVarHead pred)
+                 (predIrredErr pred)
 
          -- Make sure it is OK to have an irred pred in this context
          -- See Note [Irreducible predicates in superclasses]
-       ; checkTc (xopt Opt_UndecidableInstances dflags || not (dodgy_superclass ctxt))
-                 (predIrredBadCtxtErr pred) }
+       ; failIfTc (is_superclass ctxt
+                   && not (xopt Opt_UndecidableInstances dflags)
+                   && has_tyfun_head pred)
+                  (predSuperClassErr pred) }
   where
-    dodgy_superclass ctxt
-       = case ctxt of { ClassSCCtxt _ -> True; InstDeclCtxt -> True; _ -> False }
+    is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
+    has_tyfun_head ty
+      = case tcSplitTyConApp_maybe ty of
+          Just (tc, _) -> isTypeFamilyTyCon tc
+          Nothing      -> False
 
 {- Note [ConstraintKinds in predicates]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -679,7 +689,7 @@ e.g.   module A where
 
 Note [Irreducible predicates in superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Allowing irreducible predicates in class superclasses is somewhat dangerous
+Allowing type-family calls in class superclasses is somewhat dangerous
 because we can write:
 
  type family Fooish x :: * -> Constraint
@@ -688,10 +698,7 @@ because we can write:
 
 This will cause the constraint simplifier to loop because every time we canonicalise a
 (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
-solved to add+canonicalise another (Foo a) constraint.
-
-It is equally dangerous to allow them in instance heads because in that case the
-Paterson conditions may not detect duplication of a type variable or size change. -}
+solved to add+canonicalise another (Foo a) constraint.  -}
 
 -------------------------
 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
@@ -722,10 +729,25 @@ check_class_pred dflags ctxt pred cls tys
 -------------------------
 okIPCtxt :: UserTypeCtxt -> Bool
   -- See Note [Implicit parameters in instance decls]
+okIPCtxt (FunSigCtxt {})    = True
+okIPCtxt (InfSigCtxt {})    = True
+okIPCtxt ExprSigCtxt        = True
+okIPCtxt PatSigCtxt         = True
+okIPCtxt ResSigCtxt         = True
+okIPCtxt GenSigCtxt         = True
+okIPCtxt (ConArgCtxt {})    = True
+okIPCtxt (ForSigCtxt {})    = True  -- ??
+okIPCtxt ThBrackCtxt        = True
+okIPCtxt GhciCtxt           = True
+okIPCtxt SigmaCtxt          = True
+okIPCtxt (DataTyCtxt {})    = True
+
 okIPCtxt (ClassSCCtxt {})  = False
 okIPCtxt (InstDeclCtxt {}) = False
 okIPCtxt (SpecInstCtxt {}) = False
-okIPCtxt _                 = True
+okIPCtxt (TySynCtxt {})    = False
+okIPCtxt (RuleSigCtxt {})  = False
+okIPCtxt DefaultDeclCtxt   = False
 
 badIPPred :: PredType -> SDoc
 badIPPred pred = ptext (sLit "Illegal implicit parameter") <+> quotes (ppr pred)
@@ -756,10 +778,9 @@ checkThetaCtxt ctxt theta
   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
           ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]
 
-eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predIrredBadCtxtErr :: PredType -> SDoc
-eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprType pred
-                    $$
-                    parens (ptext (sLit "Use GADTs or TypeFamilies to permit this"))
+eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predSuperClassErr :: PredType -> SDoc
+eqPredTyErr  pred  = vcat [ ptext (sLit "Illegal equational constraint") <+> pprType pred
+                          , parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) ]
 predTyVarErr pred  = vcat [ hang (ptext (sLit "Non type-variable argument"))
                                2 (ptext (sLit "in the constraint:") <+> pprType pred)
                           , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
@@ -767,9 +788,10 @@ predTupleErr pred  = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType
                         2 (parens constraintKindsMsg)
 predIrredErr pred  = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)
                         2 (parens constraintKindsMsg)
-predIrredBadCtxtErr pred = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
-                                 <+> ptext (sLit "in a superclass/instance context"))
-                               2 (parens undecidableMsg)
+predSuperClassErr pred
+  = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred)
+          <+> ptext (sLit "in a superclass context"))
+       2 (parens undecidableMsg)
 
 constraintSynErr :: Type -> SDoc
 constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))
@@ -886,10 +908,9 @@ not converge.  See Trac #5287.
 validDerivPred :: TyVarSet -> PredType -> Bool
 validDerivPred tv_set pred
   = case classifyPredType pred of
-       ClassPred _ tys       -> check_tys tys
-       TuplePred ps          -> all (validDerivPred tv_set) ps
-       EqPred {}             -> False  -- reject equality constraints
-       _                     -> True   -- Non-class predicates are ok
+       ClassPred _ tys -> check_tys tys
+       EqPred {}       -> False  -- reject equality constraints
+       _               -> True   -- Non-class predicates are ok
   where
     check_tys tys = hasNoDups fvs
                     && sizeTypes tys == fromIntegral (length fvs)
@@ -963,6 +984,9 @@ The underlying idea is that
     context has fewer type constructors than the head.
 -}
 
+leafTyConKeys :: [Unique]
+leafTyConKeys = [eqTyConKey, coercibleTyConKey, ipClassNameKey]
+
 checkInstTermination :: [TcType] -> ThetaType -> TcM ()
 -- See Note [Paterson conditions]
 checkInstTermination tys theta
@@ -976,36 +1000,45 @@ checkInstTermination tys theta
 
    check :: PredType -> TcM ()
    check pred
-     = case classifyPredType pred of
-         TuplePred preds -> check_preds preds  -- Look inside tuple predicates; Trac #8359
-         EqPred {}       -> return ()          -- You can't get from equalities
-                                               -- to class predicates, so this is safe
-         _other      -- ClassPred, IrredPred
-           | not (null bad_tvs)
-           -> addErrTc (predUndecErr pred (nomoreMsg bad_tvs) $$ parens undecidableMsg)
-           | sizePred pred >= size
-           -> addErrTc (predUndecErr pred smallerMsg $$ parens undecidableMsg)
-           | otherwise
-           -> return ()
+     = case tcSplitTyConApp_maybe pred of
+         Just (tc, tys)
+           | getUnique tc `elem` leafTyConKeys
+           -> return ()  -- You can't get from equalities or implicit
+                         -- params to class predicates, so this is safe
+
+           | isTupleTyCon tc
+           -> check_preds tys
+              -- Look inside tuple predicates; Trac #8359
+
+         _other      -- All others: other ClassPreds, IrredPred
+           | not (null bad_tvs)    -> addErrTc (noMoreMsg bad_tvs what)
+           | sizePred pred >= size -> addErrTc (smallerMsg what)
+           | otherwise             -> return ()
      where
+        what    = ptext (sLit "constraint") <+> quotes (ppr pred)
         bad_tvs = filterOut isKindVar (fvType pred \\ fvs)
              -- Rightly or wrongly, we only check for
              -- excessive occurrences of *type* variables.
              -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
 
-predUndecErr :: PredType -> SDoc -> SDoc
-predUndecErr pred msg = sep [msg,
-                        nest 2 (ptext (sLit "in the constraint:") <+> pprType pred)]
-
-nomoreMsg :: [TcTyVar] -> SDoc
-nomoreMsg tvs
-  = sep [ ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs)
-        , (if isSingleton tvs then ptext (sLit "occurs")
-                                  else ptext (sLit "occur"))
-          <+> ptext (sLit "more often than in the instance head") ]
+smallerMsg :: SDoc -> SDoc
+smallerMsg what
+  = vcat [ hang (ptext (sLit "The") <+> what)
+              2 (ptext (sLit "is no smaller than the instance head"))
+         , parens undecidableMsg ]
+
+noMoreMsg :: [TcTyVar] -> SDoc -> SDoc
+noMoreMsg tvs what
+  = vcat [ hang (ptext (sLit "Variable") <> plural tvs <+> quotes (pprWithCommas ppr tvs)
+                <+> occurs <+> ptext (sLit "more often"))
+              2 (sep [ ptext (sLit "in the") <+> what
+                     , ptext (sLit "than in the instance head") ])
+         , parens undecidableMsg ]
+  where
+   occurs = if isSingleton tvs then ptext (sLit "occurs")
+                               else ptext (sLit "occur")
 
-smallerMsg, undecidableMsg, constraintKindsMsg :: SDoc
-smallerMsg         = ptext (sLit "Constraint is no smaller than the instance head")
+undecidableMsg, constraintKindsMsg :: SDoc
 undecidableMsg     = ptext (sLit "Use UndecidableInstances to permit this")
 constraintKindsMsg = ptext (sLit "Use ConstraintKinds to permit this")
 
@@ -1192,16 +1225,12 @@ checkFamInstRhs lhsTys famInsts
    size = sizeTypes lhsTys
    fvs  = fvTypes lhsTys
    check (tc, tys)
-      | not (all isTyFamFree tys)
-      = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
-      | not (null bad_tvs)
-      = Just (famInstUndecErr famInst (nomoreMsg bad_tvs) $$ parens undecidableMsg)
-      | size <= sizeTypes tys
-      = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
-      | otherwise
-      = Nothing
+      | not (all isTyFamFree tys) = Just (nestedMsg what)
+      | not (null bad_tvs)        = Just (noMoreMsg bad_tvs what)
+      | size <= sizeTypes tys     = Just (smallerMsg what)
+      | otherwise                 = Nothing
       where
-        famInst = TyConApp tc tys
+        what    = ptext (sLit "type family application") <+> quotes (pprType (TyConApp tc tys))
         bad_tvs = filterOut isKindVar (fvTypes tys \\ fvs)
              -- Rightly or wrongly, we only check for
              -- excessive occurrences of *type* variables.
@@ -1247,11 +1276,10 @@ tyFamInstIllegalErr ty
          colon) 2 $
       ppr ty
 
-famInstUndecErr :: Type -> SDoc -> SDoc
-famInstUndecErr ty msg
-  = sep [msg,
-         nest 2 (ptext (sLit "in the type family application:") <+>
-                 pprType ty)]
+nestedMsg :: SDoc -> SDoc
+nestedMsg what
+  = sep [ ptext (sLit "Illegal nested") <+> what
+        , parens undecidableMsg ]
 
 famPatErr :: TyCon -> [TyVar] -> [Type] -> SDoc
 famPatErr fam_tc tvs pats
@@ -1260,10 +1288,6 @@ famPatErr fam_tc tvs pats
        2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
              2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
 
-nestedMsg, smallerAppMsg :: SDoc
-nestedMsg     = ptext (sLit "Nested type family application")
-smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1331,14 +1355,14 @@ sizeTypes xs = sum (map sizeType tys)
 -- "local instances" in expressions).
 -- See Trac #4200.
 sizePred :: PredType -> TypeSize
-sizePred p = go (classifyPredType p)
-  where
-    go (ClassPred cls tys')
-      | isIPClass cls     = 0  -- See Note [Size of a predicate]
-      | otherwise         = sizeTypes tys'
-    go (EqPred {})        = 0  -- See Note [Size of a predicate]
-    go (TuplePred ts)     = sum (map sizePred ts)
-    go (IrredPred ty)     = sizeType ty
+sizePred p
+  = case classifyPredType p of
+      ClassPred cls tys
+        | isIPClass cls     -> 0  -- See Note [Size of a predicate]
+        | isCTupleClass cls -> maximum (0 : map sizePred tys)
+        | otherwise         -> sizeTypes tys
+      EqPred {}             -> 0  -- See Note [Size of a predicate]
+      IrredPred ty          -> sizeType ty
 
 {-
 ************************************************************************