Major Overhaul of Pattern Match Checking (Fixes #595)
[ghc.git] / compiler / typecheck / TcType.hs
index 9ce1449..60ab685 100644 (file)
@@ -21,15 +21,15 @@ module TcType (
   --------------------------------
   -- Types
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
-  TcTyVar, TcTyVarSet, TcKind, TcCoVar,
+  TcTyVar, TcTyVarSet, TcDTyVarSet, TcKind, TcCoVar,
 
   -- TcLevel
   TcLevel(..), topTcLevel, pushTcLevel,
-  strictlyDeeperThan, sameDepthAs, fskTcLevel,
+  strictlyDeeperThan, sameDepthAs, fmvTcLevel,
 
   --------------------------------
   -- MetaDetails
-  UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt,
+  UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt, isSigMaybe,
   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
   MetaDetails(Flexi, Indirect), MetaInfo(..),
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
@@ -63,13 +63,14 @@ module TcType (
   -- Predicates.
   -- Again, newtypes are opaque
   eqType, eqTypes, eqPred, cmpType, cmpTypes, cmpPred, eqTypeX,
-  pickyEqType, tcEqType, tcEqKind,
+  tcEqType, tcEqKind,
   isSigmaTy, isRhoTy, isOverloadedTy,
-  isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
+  isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
-  isPredTy, isTyVarClassPred, isTyVarExposed,
+  isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
   checkValidClsArgs, hasTyVarHead,
+  isRigidEqPred, isRigidTy,
 
   ---------------------------------
   -- Misc type manipulators
@@ -81,7 +82,7 @@ module TcType (
 
   ---------------------------------
   -- Predicate types
-  mkMinimalBySCs, transSuperClasses, transSuperClassesPred, 
+  mkMinimalBySCs, transSuperClasses, transSuperClassesPred,
   immSuperClasses,
   isImprovementPred,
 
@@ -142,11 +143,22 @@ module TcType (
   isPrimitiveType,
 
   tyVarsOfType, tyVarsOfTypes, closeOverKinds,
+  tyVarsOfTypeList, tyVarsOfTypesList,
+  tyVarsOfTypeAcc, tyVarsOfTypesAcc,
+  tyVarsOfTypeDSet, tyVarsOfTypesDSet, closeOverKindsDSet,
   tcTyVarsOfType, tcTyVarsOfTypes,
 
+  --------------------------------
+  -- Transforming Types to TcTypes
+  toTcType,    -- :: Type -> TcType
+  toTcTyVar,   -- :: TyVar -> TcTyVar
+  toTcTypeBag, -- :: Bag EvVar -> Bag EvVar
+
   pprKind, pprParendKind, pprSigmaType,
   pprType, pprParendType, pprTypeApp, pprTyThingCategory,
-  pprTheta, pprThetaArrowTy, pprClassPred
+  pprTheta, pprThetaArrowTy, pprClassPred,
+
+  TypeSize, sizeType, sizeTypes
 
   ) where
 
@@ -175,11 +187,12 @@ import PrelNames
 import TysWiredIn
 import BasicTypes
 import Util
+import Bag
 import Maybes
 import ListSetOps
 import Outputable
 import FastString
-import ErrUtils( Validity(..), isValid )
+import ErrUtils( Validity(..), MsgDoc, isValid )
 
 import Data.IORef
 import Control.Monad (liftM, ap)
@@ -240,6 +253,7 @@ type TcRhoType      = TcType  -- Note [TcRhoType]
 type TcTauType      = TcType
 type TcKind         = Kind
 type TcTyVarSet     = TyVarSet
+type TcDTyVarSet    = DTyVarSet
 
 {-
 Note [TcRhoType]
@@ -343,11 +357,9 @@ instance Outputable MetaDetails where
   ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
 
 data MetaInfo
-   = TauTv Bool    -- This MetaTv is an ordinary unification variable
+   = TauTv         -- This MetaTv is an ordinary unification variable
                    -- A TauTv is always filled in with a tau-type, which
                    -- never contains any ForAlls.
-                   -- The boolean is true when the meta var originates
-                   -- from a wildcard.
 
    | ReturnTv      -- Can unify with *anything*. Used to convert a
                    -- type "checking" algorithm into a type inference algorithm.
@@ -369,16 +381,25 @@ data MetaInfo
 -- in the places where we need to an expression has that type
 
 data UserTypeCtxt
-  = FunSigCtxt Name Bool    -- Function type signature, when checking the type
-                            -- Also used for types in SPECIALISE pragmas
-                            -- Bool = True  <=> report redundant class constraints
-                            --        False <=> do not
-                            -- See Note [Tracking redundant constraints] in TcSimplify
+  = FunSigCtxt      -- Function type signature, when checking the type
+                    -- Also used for types in SPECIALISE pragmas
+       Name              -- Name of the function
+       Bool              -- True <=> report redundant constraints
+                            -- This is usually True, but False for
+                            --   * Record selectors (not important here)
+                            --   * Class and instance methods.  Here
+                            --     the code may legitimately be more
+                            --     polymorphic than the signature
+                            --     generated from the class
+                            --     declaration
 
   | InfSigCtxt Name     -- Inferred type for function
   | ExprSigCtxt         -- Expression type signature
+
   | ConArgCtxt Name     -- Data constructor argument
   | TySynCtxt Name      -- RHS of a type synonym decl
+  | PatSynCtxt Name     -- Type sig for a pattern synonym
+                        --   eg  pattern C :: Int -> T
   | PatSigCtxt          -- Type sig in pattern
                         --   eg  f (x::t) = ...
                         --   or  (x::t, y) = e
@@ -412,17 +433,18 @@ data UserTypeCtxt
 -- will become  type T = forall a. a->a
 --
 -- With gla-exts that's right, but for H98 we should complain.
+-}
 
 
-************************************************************************
+{- *********************************************************************
 *                                                                      *
                 Untoucable type variables
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
 
 newtype TcLevel = TcLevel Int deriving( Eq, Ord )
   -- See Note [TcLevel and untouchable type variables] for what this Int is
+  -- See also Note [TcLevel assignment]
 
 {-
 Note [TcLevel and untouchable type variables]
@@ -448,7 +470,6 @@ Note [TcLevel and untouchable type variables]
                 implication are all untouchable; ie their level
                 numbers are LESS THAN the ic_tclvl of the implication
 
-
 Note [Skolem escape prevention]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We only unify touchable unification variables.  Because of
@@ -481,17 +502,36 @@ emerges. If we (wrongly) spontaneously solved it to get uf := beta,
 the whole implication disappears but when we pop out again we are left with
 (F Int ~ uf) which will be unified by our final zonking stage and
 uf will get unified *once more* to (F Int).
+
+Note [TcLevel assignment]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+We arrange the TcLevels like this
+
+   1   Top level
+   2     Flatten-meta-vars of level 3
+   3   First-level implication constraints
+   4     Flatten-meta-vars of level 5
+   5   Second-level implication constraints
+   ...etc...
+
+The even-numbered levels are for the flatten-meta-variables assigned
+at the next level in.  Eg for a second-level implication conststraint
+(level 5), the flatten meta-vars are level 4, which makes them untouchable.
+The flatten meta-vars could equally well all have level 0, or just NotALevel
+since they do not live across implications.
 -}
 
-fskTcLevel :: TcLevel
-fskTcLevel = TcLevel 0  -- 0 = Outside the outermost level:
-                                  --     flatten skolems
+fmvTcLevel :: TcLevel -> TcLevel
+-- See Note [TcLevel assignment]
+fmvTcLevel (TcLevel n) = TcLevel (n-1)
 
 topTcLevel :: TcLevel
+-- See Note [TcLevel assignment]
 topTcLevel = TcLevel 1   -- 1 = outermost level
 
 pushTcLevel :: TcLevel -> TcLevel
-pushTcLevel (TcLevel us) = TcLevel (us+1)
+-- See Note [TcLevel assignment]
+pushTcLevel (TcLevel us) = TcLevel (us + 2)
 
 strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
 strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
@@ -528,11 +568,10 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
   = pp_info <> colon <> ppr tclvl
   where
     pp_info = case info of
-                ReturnTv    -> ptext (sLit "ret")
-                TauTv True  -> ptext (sLit "twc")
-                TauTv False -> ptext (sLit "tau")
-                SigTv       -> ptext (sLit "sig")
-                FlatMetaTv  -> ptext (sLit "fuv")
+                ReturnTv   -> ptext (sLit "ret")
+                TauTv      -> ptext (sLit "tau")
+                SigTv      -> ptext (sLit "sig")
+                FlatMetaTv -> ptext (sLit "fuv")
 
 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
 pprUserTypeCtxt (FunSigCtxt n _)  = ptext (sLit "the type signature for") <+> quotes (ppr n)
@@ -541,6 +580,7 @@ pprUserTypeCtxt (RuleSigCtxt n)   = ptext (sLit "a RULE for") <+> quotes (ppr n)
 pprUserTypeCtxt ExprSigCtxt       = ptext (sLit "an expression type signature")
 pprUserTypeCtxt (ConArgCtxt c)    = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
 pprUserTypeCtxt (TySynCtxt c)     = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
+pprUserTypeCtxt (PatSynCtxt c)    = ptext (sLit "the type signature for pattern synonym") <+> quotes (ppr c)
 pprUserTypeCtxt ThBrackCtxt       = ptext (sLit "a Template Haskell quotation [t|...|]")
 pprUserTypeCtxt PatSigCtxt        = ptext (sLit "a pattern type signature")
 pprUserTypeCtxt ResSigCtxt        = ptext (sLit "a result type signature")
@@ -560,15 +600,22 @@ pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
 --              f :: <type>
 -- The <extra> is either empty or "the ambiguity check for"
 pprSigCtxt ctxt extra pp_ty
-  = sep [ ptext (sLit "In") <+> extra <+> pprUserTypeCtxt ctxt <> colon
-        , nest 2 (pp_sig ctxt) ]
+  | Just n <- isSigMaybe ctxt
+  = vcat [ ptext (sLit "In") <+> extra <+> ptext (sLit "the type signature:")
+         , nest 2 (pprPrefixOcc n <+> dcolon <+> pp_ty) ]
+
+  | otherwise
+  = hang (ptext (sLit "In") <+> extra <+> pprUserTypeCtxt ctxt <> colon)
+       2 pp_ty
+
   where
-    pp_sig (FunSigCtxt n _) = pp_n_colon n
-    pp_sig (ConArgCtxt n)   = pp_n_colon n
-    pp_sig (ForSigCtxt n)   = pp_n_colon n
-    pp_sig _                = pp_ty
 
-    pp_n_colon n = pprPrefixOcc n <+> dcolon <+> pp_ty
+isSigMaybe :: UserTypeCtxt -> Maybe Name
+isSigMaybe (FunSigCtxt n _) = Just n
+isSigMaybe (ConArgCtxt n)   = Just n
+isSigMaybe (ForSigCtxt n)   = Just n
+isSigMaybe (PatSynCtxt n)   = Just n
+isSigMaybe _                = Nothing
 
 {-
 ************************************************************************
@@ -1137,26 +1184,6 @@ tcEqType ty1 ty2
     gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
     gos _ _ _ = False
 
-pickyEqType :: TcType -> TcType -> Bool
--- Check when two types _look_ the same, _including_ synonyms.
--- So (pickyEqType String [Char]) returns False
-pickyEqType ty1 ty2
-  = go init_env ty1 ty2
-  where
-    init_env = mkRnEnv2 (mkInScopeSet (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
-    go env (TyVarTy tv1)       (TyVarTy tv2)     = rnOccL env tv1 == rnOccR env tv2
-    go _   (LitTy lit1)        (LitTy lit2)      = lit1 == lit2
-    go env (ForAllTy tv1 t1)   (ForAllTy tv2 t2) = go env (tyVarKind tv1) (tyVarKind tv2)
-                                                && go (rnBndr2 env tv1 tv2) t1 t2
-    go env (AppTy s1 t1)       (AppTy s2 t2)     = go env s1 s2 && go env t1 t2
-    go env (FunTy s1 t1)       (FunTy s2 t2)     = go env s1 s2 && go env t1 t2
-    go env (TyConApp tc1 ts1) (TyConApp tc2 ts2) = (tc1 == tc2) && gos env ts1 ts2
-    go _ _ _ = False
-
-    gos _   []       []       = True
-    gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
-    gos _ _ _ = False
-
 {-
 Note [Occurs check expansion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1193,11 +1220,11 @@ instance Functor OccCheckResult where
       fmap = liftM
 
 instance Applicative OccCheckResult where
-      pure = return
+      pure = OC_OK
       (<*>) = ap
 
 instance Monad OccCheckResult where
-  return x = OC_OK x
+  return            = pure
   OC_OK x     >>= k = k x
   OC_Forall   >>= _ = OC_Forall
   OC_NonTyVar >>= _ = OC_NonTyVar
@@ -1269,8 +1296,8 @@ occurCheckExpand dflags tv ty
     -- it and try again.
     go ty@(TyConApp tc tys)
       = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
-          OC_OK ty 
-              | impredicative || isTauTyCon tc 
+          OC_OK ty
+              | impredicative || isTauTyCon tc
               -> return ty  -- First try to eliminate the tyvar from the args
               | otherwise
               -> OC_Forall  -- A type synonym with a forall on the RHS
@@ -1283,7 +1310,7 @@ canUnifyWithPolyType dflags details kind
   = case details of
       MetaTv { mtv_info = ReturnTv } -> True      -- See Note [ReturnTv]
       MetaTv { mtv_info = SigTv }    -> False
-      MetaTv { mtv_info = TauTv _ }  -> xopt Opt_ImpredicativeTypes dflags
+      MetaTv { mtv_info = TauTv }    -> xopt Opt_ImpredicativeTypes dflags
                                      || isOpenTypeKind kind
                                           -- Note [OpenTypeKind accepts foralls]
       _other                         -> True
@@ -1320,7 +1347,7 @@ Note [Kind polymorphic type classes]
     class C f where...   -- C :: forall k. k -> Constraint
     g :: forall (f::*). C f => f -> f
 
-Here the (C f) in the signature is really (C * f), and we 
+Here the (C f) in the signature is really (C * f), and we
 don't want to complain that the * isn't a type variable!
 -}
 
@@ -1341,7 +1368,7 @@ checkValidClsArgs flexible_contexts kts
   | otherwise         = all hasTyVarHead tys
   where
     (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
-   
+
 hasTyVarHead :: Type -> Bool
 -- Returns true of (a t1 .. tn), where 'a' is a type variable
 hasTyVarHead ty                 -- Haskell 98 allows predicates of form
@@ -1399,7 +1426,7 @@ immSuperClasses cls tys
 
 isImprovementPred :: PredType -> Bool
 -- Either it's an equality, or has some functional dependency
-isImprovementPred ty 
+isImprovementPred ty
   = case classifyPredType ty of
       EqPred NomEq t1 t2 -> not (t1 `tcEqType` t2)
       EqPred ReprEq _ _  -> False
@@ -1449,6 +1476,11 @@ isUnitTy       = is_tc unitTyConKey
 isCharTy       = is_tc charTyConKey
 isAnyTy        = is_tc anyTyConKey
 
+-- | Does a type represent a floating-point number?
+isFloatingTy :: Type -> Bool
+isFloatingTy ty = isFloatTy ty || isDoubleTy ty
+
+-- | Is a type 'String'?
 isStringTy :: Type -> Bool
 isStringTy ty
   = case tcSplitTyConApp_maybe ty of
@@ -1476,6 +1508,82 @@ isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
                                  || isTyVarExposed tv arg
 isTyVarExposed _  (ForAllTy {})   = False
 
+-- | Does the given tyvar appear under a type generative w.r.t.
+-- representational equality? See Note [Occurs check error] in
+-- TcCanonical for the motivation for this function.
+isTyVarUnderDatatype :: TcTyVar -> TcType -> Bool
+isTyVarUnderDatatype tv = go False
+  where
+    go under_dt ty | Just ty' <- tcView ty = go under_dt ty'
+    go under_dt (TyVarTy tv') = under_dt && (tv == tv')
+    go under_dt (TyConApp tc tys) = let under_dt' = under_dt ||
+                                                    isGenerativeTyCon tc
+                                                      Representational
+                                    in any (go under_dt') tys
+    go _        (LitTy {}) = False
+    go _        (FunTy arg res) = go True arg || go True res
+    go under_dt (AppTy fun arg) = go under_dt fun || go under_dt arg
+    go under_dt (ForAllTy tv' inner_ty)
+      | tv' == tv = False
+      | otherwise = go under_dt inner_ty
+
+isRigidTy :: TcType -> Bool
+isRigidTy ty
+  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
+  | Just {} <- tcSplitAppTy_maybe ty        = True
+  | isForAllTy ty                           = True
+  | otherwise                               = False
+
+isRigidEqPred :: TcLevel -> PredTree -> Bool
+-- ^ True of all Nominal equalities that are solidly insoluble
+-- This means all equalities *except*
+--   * Meta-tv non-SigTv on LHS
+--   * Meta-tv SigTv on LHS, tyvar on right
+isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
+  | Just tv1 <- tcGetTyVar_maybe ty1
+  = ASSERT2( isTcTyVar tv1, ppr tv1 )
+    not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
+
+  | otherwise  -- LHS is not a tyvar
+  = True
+
+isRigidEqPred _ _ = False  -- Not an equality
+
+{-
+************************************************************************
+*                                                                      *
+\subsection{Transformation of Types to TcTypes}
+*                                                                      *
+************************************************************************
+-}
+
+toTcType :: Type -> TcType
+toTcType ty = to_tc_type emptyVarSet ty
+   where
+    to_tc_type :: VarSet -> Type -> TcType
+    -- The constraint solver expects EvVars to have TcType, in which the
+    -- free type variables are TcTyVars. So we convert from Type to TcType here
+    -- A bit tiresome; but one day I expect the two types to be entirely separate
+    -- in which case we'll definitely need to do this
+    to_tc_type forall_tvs (TyVarTy tv)
+      | Just var <- lookupVarSet forall_tvs tv = TyVarTy var
+      | otherwise = TyVarTy (toTcTyVar tv)
+    to_tc_type  ftvs (FunTy t1 t2)     = FunTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
+    to_tc_type  ftvs (AppTy t1 t2)     = AppTy (to_tc_type ftvs t1) (to_tc_type ftvs t2)
+    to_tc_type  ftvs (TyConApp tc tys) = TyConApp tc (map (to_tc_type ftvs) tys)
+    to_tc_type  ftvs (ForAllTy tv ty)  = let tv' = toTcTyVar tv
+                                         in ForAllTy tv' (to_tc_type (ftvs `extendVarSet` tv') ty)
+    to_tc_type _ftvs (LitTy l)         = LitTy l
+
+toTcTyVar :: TyVar -> TcTyVar
+toTcTyVar tv
+  | isTcTyVar tv = setVarType tv (toTcType (tyVarKind tv))
+  | isId tv      = pprPanic "toTcTyVar: Id:" (ppr tv)
+  | otherwise    = mkTcTyVar (tyVarName tv) (toTcType (tyVarKind tv)) vanillaSkolemTv
+
+toTcTypeBag :: Bag EvVar -> Bag EvVar -- All TyVars are transformed to TcTyVars
+toTcTypeBag evvars = mapBag (\tv -> setTyVarKind tv (toTcType (tyVarKind tv))) evvars
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1568,8 +1676,9 @@ orphNamesOfCoCon :: CoAxiom br -> NameSet
 orphNamesOfCoCon (CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
   = orphNamesOfTyCon tc `unionNameSet` orphNamesOfCoAxBranches branches
 
-orphNamesOfCoAxBranches :: BranchList CoAxBranch br -> NameSet
-orphNamesOfCoAxBranches = brListFoldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet
+orphNamesOfCoAxBranches :: Branches br -> NameSet
+orphNamesOfCoAxBranches
+  = foldr (unionNameSet . orphNamesOfCoAxBranch) emptyNameSet . fromBranches
 
 orphNamesOfCoAxBranch :: CoAxBranch -> NameSet
 orphNamesOfCoAxBranch (CoAxBranch { cab_lhs = lhs, cab_rhs = rhs })
@@ -1601,23 +1710,23 @@ tcSplitIOType_maybe ty
 
 isFFITy :: Type -> Bool
 -- True for any TyCon that can possibly be an arg or result of an FFI call
-isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty empty)
+isFFITy ty = isValid (checkRepTyCon legalFFITyCon ty)
 
 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Validity
 -- Checks for valid argument type for a 'foreign import'
 isFFIArgumentTy dflags safety ty
-   = checkRepTyCon (legalOutgoingTyCon dflags safety) ty empty
+   = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
 
 isFFIExternalTy :: Type -> Validity
 -- Types that are allowed as arguments of a 'foreign export'
-isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty empty
+isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
 
 isFFIImportResultTy :: DynFlags -> Type -> Validity
 isFFIImportResultTy dflags ty
-  = checkRepTyCon (legalFIResultTyCon dflags) ty empty
+  = checkRepTyCon (legalFIResultTyCon dflags) ty
 
 isFFIExportResultTy :: Type -> Validity
-isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty empty
+isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 
 isFFIDynTy :: Type -> Type -> Validity
 -- The type in a foreign import dynamic must be Ptr, FunPtr, or a newtype of
@@ -1638,10 +1747,12 @@ isFFIDynTy expected ty
 
 isFFILabelTy :: Type -> Validity
 -- The type of a foreign label must be Ptr, FunPtr, or a newtype of either.
-isFFILabelTy ty = checkRepTyCon ok ty extra
+isFFILabelTy ty = checkRepTyCon ok ty
   where
-    ok tc = tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
-    extra = ptext (sLit "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)")
+    ok tc | tc `hasKey` funPtrTyConKey || tc `hasKey` ptrTyConKey
+          = IsValid
+          | otherwise
+          = NotValid (ptext (sLit "A foreign-imported address (via &foo) must have type (Ptr a) or (FunPtr a)"))
 
 isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
 -- Checks for valid argument type for a 'foreign import prim'
@@ -1650,28 +1761,35 @@ isFFIPrimArgumentTy :: DynFlags -> Type -> Validity
 -- the foreign function.
 isFFIPrimArgumentTy dflags ty
   | isAnyTy ty = IsValid
-  | otherwise  = checkRepTyCon (legalFIPrimArgTyCon dflags) ty empty
+  | otherwise  = checkRepTyCon (legalFIPrimArgTyCon dflags) ty
 
 isFFIPrimResultTy :: DynFlags -> Type -> Validity
 -- Checks for valid result type for a 'foreign import prim'
--- Currently it must be an unlifted type, including unboxed tuples.
+-- Currently it must be an unlifted type, including unboxed tuples,
+-- or the well-known type Any.
 isFFIPrimResultTy dflags ty
-   = checkRepTyCon (legalFIPrimResultTyCon dflags) ty empty
+  | isAnyTy ty = IsValid
+  | otherwise = checkRepTyCon (legalFIPrimResultTyCon dflags) ty
 
 isFunPtrTy :: Type -> Bool
-isFunPtrTy ty = isValid (checkRepTyCon (`hasKey` funPtrTyConKey) ty empty)
+isFunPtrTy ty
+  | Just (tc, [_]) <- splitTyConApp_maybe ty
+  = tc `hasKey` funPtrTyConKey
+  | otherwise
+  = False
 
 -- normaliseFfiType gets run before checkRepTyCon, so we don't
 -- need to worry about looking through newtypes or type functions
 -- here; that's already been taken care of.
-checkRepTyCon :: (TyCon -> Bool) -> Type -> SDoc -> Validity
-checkRepTyCon check_tc ty extra
+checkRepTyCon :: (TyCon -> Validity) -> Type -> Validity
+checkRepTyCon check_tc ty
   = case splitTyConApp_maybe ty of
       Just (tc, tys)
         | isNewTyCon tc -> NotValid (hang msg 2 (mk_nt_reason tc tys $$ nt_fix))
-        | check_tc tc   -> IsValid
-        | otherwise     -> NotValid (msg $$ extra)
-      Nothing -> NotValid (quotes (ppr ty) <+> ptext (sLit "is not a data type") $$ extra)
+        | otherwise     -> case check_tc tc of
+                             IsValid        -> IsValid
+                             NotValid extra -> NotValid (msg $$ extra)
+      Nothing -> NotValid (quotes (ppr ty) <+> ptext (sLit "is not a data type"))
   where
     msg = quotes (ppr ty) <+> ptext (sLit "cannot be marshalled in a foreign call")
     mk_nt_reason tc tys
@@ -1701,47 +1819,46 @@ These chaps do the work; they are not exported
 ----------------------------------------------
 -}
 
-legalFEArgTyCon :: TyCon -> Bool
+legalFEArgTyCon :: TyCon -> Validity
 legalFEArgTyCon tc
   -- It's illegal to make foreign exports that take unboxed
   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
   = boxedMarshalableTyCon tc
 
-legalFIResultTyCon :: DynFlags -> TyCon -> Bool
+legalFIResultTyCon :: DynFlags -> TyCon -> Validity
 legalFIResultTyCon dflags tc
-  | tc == unitTyCon         = True
+  | tc == unitTyCon         = IsValid
   | otherwise               = marshalableTyCon dflags tc
 
-legalFEResultTyCon :: TyCon -> Bool
+legalFEResultTyCon :: TyCon -> Validity
 legalFEResultTyCon tc
-  | tc == unitTyCon         = True
+  | tc == unitTyCon         = IsValid
   | otherwise               = boxedMarshalableTyCon tc
 
-legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
+legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Validity
 -- Checks validity of types going from Haskell -> external world
 legalOutgoingTyCon dflags _ tc
   = marshalableTyCon dflags tc
 
-legalFFITyCon :: TyCon -> Bool
+legalFFITyCon :: TyCon -> Validity
 -- True for any TyCon that can possibly be an arg or result of an FFI call
 legalFFITyCon tc
-  | isUnLiftedTyCon tc = True
-  | tc == unitTyCon    = True
+  | isUnLiftedTyCon tc = IsValid
+  | tc == unitTyCon    = IsValid
   | otherwise          = boxedMarshalableTyCon tc
 
-marshalableTyCon :: DynFlags -> TyCon -> Bool
+marshalableTyCon :: DynFlags -> TyCon -> Validity
 marshalableTyCon dflags tc
-  |  (xopt Opt_UnliftedFFITypes dflags
-      && isUnLiftedTyCon tc
-      && not (isUnboxedTupleTyCon tc)
-      && case tyConPrimRep tc of        -- Note [Marshalling VoidRep]
-           VoidRep -> False
-           _       -> True)
-  = True
+  | isUnLiftedTyCon tc
+  , not (isUnboxedTupleTyCon tc)
+  , case tyConPrimRep tc of        -- Note [Marshalling VoidRep]
+       VoidRep -> False
+       _       -> True
+  = validIfUnliftedFFITypes dflags
   | otherwise
   = boxedMarshalableTyCon tc
 
-boxedMarshalableTyCon :: TyCon -> Bool
+boxedMarshalableTyCon :: TyCon -> Validity
 boxedMarshalableTyCon tc
    | getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
                          , int32TyConKey, int64TyConKey
@@ -1753,35 +1870,42 @@ boxedMarshalableTyCon tc
                          , stablePtrTyConKey
                          , boolTyConKey
                          ]
-  = True
+  = IsValid
 
-  | otherwise = False
+  | otherwise = NotValid empty
 
-legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
+legalFIPrimArgTyCon :: DynFlags -> TyCon -> Validity
 -- Check args of 'foreign import prim', only allow simple unlifted types.
 -- Strictly speaking it is unnecessary to ban unboxed tuples here since
 -- currently they're of the wrong kind to use in function args anyway.
 legalFIPrimArgTyCon dflags tc
-  | xopt Opt_UnliftedFFITypes dflags
-    && isUnLiftedTyCon tc
-    && not (isUnboxedTupleTyCon tc)
-  = True
+  | isUnLiftedTyCon tc
+  , not (isUnboxedTupleTyCon tc)
+  = validIfUnliftedFFITypes dflags
   | otherwise
-  = False
+  = NotValid unlifted_only
 
-legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
+legalFIPrimResultTyCon :: DynFlags -> TyCon -> Validity
 -- Check result type of 'foreign import prim'. Allow simple unlifted
 -- types and also unboxed tuple result types '... -> (# , , #)'
 legalFIPrimResultTyCon dflags tc
-  | xopt Opt_UnliftedFFITypes dflags
-    && isUnLiftedTyCon tc
-    && (isUnboxedTupleTyCon tc
-        || case tyConPrimRep tc of      -- Note [Marshalling VoidRep]
+  | isUnLiftedTyCon tc
+  , (isUnboxedTupleTyCon tc
+     || case tyConPrimRep tc of      -- Note [Marshalling VoidRep]
            VoidRep -> False
            _       -> True)
-  = True
+  = validIfUnliftedFFITypes dflags
+
   | otherwise
-  = False
+  = NotValid unlifted_only
+
+unlifted_only :: MsgDoc
+unlifted_only = ptext (sLit "foreign import prim only accepts simple unlifted types")
+
+validIfUnliftedFFITypes :: DynFlags -> Validity
+validIfUnliftedFFITypes dflags
+  | xopt Opt_UnliftedFFITypes dflags =  IsValid
+  | otherwise = NotValid (ptext (sLit "To marshal unlifted types, use UnliftedFFITypes"))
 
 {-
 Note [Marshalling VoidRep]
@@ -1793,3 +1917,62 @@ In turn that means you can't write
 Reason: the back end falls over with panic "primRepHint:VoidRep";
         and there is no compelling reason to permit it
 -}
+
+{-
+************************************************************************
+*                                                                      *
+        The "Paterson size" of a type
+*                                                                      *
+************************************************************************
+-}
+
+{-
+Note [Paterson conditions on PredTypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are considering whether *class* constraints terminate
+(see Note [Paterson conditions]). Precisely, the Paterson conditions
+would have us check that "the constraint has fewer constructors and variables
+(taken together and counting repetitions) than the head.".
+
+However, we can be a bit more refined by looking at which kind of constraint
+this actually is. There are two main tricks:
+
+ 1. It seems like it should be OK not to count the tuple type constructor
+    for a PredType like (Show a, Eq a) :: Constraint, since we don't
+    count the "implicit" tuple in the ThetaType itself.
+
+    In fact, the Paterson test just checks *each component* of the top level
+    ThetaType against the size bound, one at a time. By analogy, it should be
+    OK to return the size of the *largest* tuple component as the size of the
+    whole tuple.
+
+ 2. Once we get into an implicit parameter or equality we
+    can't get back to a class constraint, so it's safe
+    to say "size 0".  See Trac #4200.
+
+NB: we don't want to detect PredTypes in sizeType (and then call
+sizePred on them), or we might get an infinite loop if that PredType
+is irreducible. See Trac #5581.
+-}
+
+type TypeSize = IntWithInf
+
+sizeType, size_type :: Type -> TypeSize
+-- Size of a type: the number of variables and constructors
+-- Ignore kinds altogether
+sizeType ty | isKind ty = 0
+            | otherwise = size_type ty
+
+size_type ty | Just exp_ty <- tcView ty = size_type exp_ty
+size_type (TyVarTy {})      = 1
+size_type (TyConApp tc tys)
+  | isTypeFamilyTyCon tc   = infinity  -- Type-family applications can
+                                       -- expand to any arbitrary size
+  | otherwise              = sizeTypes tys + 1
+size_type (LitTy {})        = 1
+size_type (FunTy arg res)   = size_type arg + size_type res + 1
+size_type (AppTy fun arg)   = size_type fun + size_type arg
+size_type (ForAllTy _ ty)   = size_type ty
+
+sizeTypes :: [Type] -> TypeSize
+sizeTypes tys = sum (map sizeType tys)