projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Adding pushing of hpc translation status through hi files.
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 11ec9d9..955d45c 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1,9 +1,12 @@
 %
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section{Monadic type operations}
 
 
-This module contains monadic operations over types that contain mutable type variables
+Monadic type operations
+
+This module contains monadic operations over types that contain
+mutable type variables
 
 \begin{code}
 module TcMType (
 
 \begin{code}
 module TcMType (
@@ -23,6 +26,10 @@ module TcMType (
   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
 
   --------------------------------
   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
 
   --------------------------------
+  -- Creating new coercion variables
+  newCoVars,
+
+  --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
   tcInstSigTyVars, zonkSigTyVar,
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
   tcInstSigTyVars, zonkSigTyVar,
@@ -40,9 +47,10 @@ module TcMType (
   --------------------------------
   -- Zonking
   zonkType, zonkTcPredType, 
   --------------------------------
   -- Zonking
   zonkType, zonkTcPredType, 
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcKindToKind, zonkTcKind,
+  zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
 
   readKindVar, writeKindVar
 
 
   readKindVar, writeKindVar
 
@@ -50,54 +58,30 @@ module TcMType (
 
 #include "HsVersions.h"
 
 
 #include "HsVersions.h"
 
-
 -- friends:
 -- friends:
-import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
-                         ThetaType
-                       ) 
-import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
-                         MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
-                         BoxyTyVar, BoxyType, UserTypeCtxt(..),
-                         isMetaTyVar, isSigTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, tcGetTyVar,
-                         tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
-                         tcValidInstHeadTy, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
-                         typeKind, isSkolemTyVar,
-                         mkAppTy, mkTyVarTy, mkTyVarTys, 
-                         tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, tcView,
-                         pprPred, pprTheta, pprClassPred )
-import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, 
-                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
-                         liftedTypeKind, defaultKind
-                       )
-import Type            ( TvSubst, zipTopTvSubst, substTy )
-import Class           ( Class, classArity, className )
-import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName )
-import Var             ( TyVar, tyVarKind, tyVarName, isTcTyVar, 
-                         mkTyVar, mkTcTyVar, tcTyVarDetails )
-
-       -- Assertions
-#ifdef DEBUG
-import TcType          ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Kind            ( isSubKind )
-#endif
+import TypeRep
+import TcType
+import Type
+import Coercion
+import Class
+import TyCon
+import Var
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
-import FunDeps         ( grow, checkInstCoverage )
-import Name            ( Name, setNameUnique, mkSysTvName )
+import FunDeps
+import Name
 import VarSet
 import VarSet
-import DynFlags                ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, notNull )
-import ListSetOps      ( removeDups )
+import ErrUtils
+import DynFlags
+import Util
+import Maybes
+import ListSetOps
+import UniqSupply
+import SrcLoc
 import Outputable
 
 import Outputable
 
-import Control.Monad   ( when )
+import Control.Monad   ( when, unless )
 import Data.List       ( (\\) )
 \end{code}
 
 import Data.List       ( (\\) )
 \end{code}
 
@@ -139,10 +123,17 @@ tcInstType inst_tyvars ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
+newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
+newCoVars spec
+  = do { us <- newUniqueSupply 
+       ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
+                          (mkCoKind ty1 ty2)
+                | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
-               ; ref <- newMutVar Nothing
-               ; return (KindVar (mkKindVar uniq ref)) }
+               ; ref <- newMutVar Flexi
+               ; return (mkTyVarTy (mkKindVar uniq ref)) }
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
@@ -170,19 +161,30 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh skolem constants
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
-
-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcInstSkolTyVar info tyvar
+tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
+-- Instantiate the tyvar, using 
+--     * the occ-name and kind of the supplied tyvar, 
+--     * the unique from the monad,
+--     * the location either from the tyvar (mb_loc = Nothing)
+--       or from mb_loc (Just loc)
+tcInstSkolTyVar info mb_loc tyvar
   = do { uniq <- newUnique
   = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-             kind = tyVarKind tyvar
-       ; return (mkSkolTyVar name kind info) }
+       ; let old_name = tyVarName tyvar
+             kind     = tyVarKind tyvar
+             loc      = mb_loc `orElse` getSrcSpan old_name
+             new_name = mkInternalName uniq (nameOccName old_name) loc
+       ; return (mkSkolTyVar new_name kind info) }
 
 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 
 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
+-- Get the location from the monad
+tcInstSkolTyVars info tyvars 
+  = do         { span <- getSrcSpanM
+       ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
+
+tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+-- Binding location comes from the monad
+tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 \end{code}
 
 
 \end{code}
 
 
@@ -285,9 +287,14 @@ tcInstTyVars tyvars
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with meta SigTvs
-tcInstSigTyVars skol_info tyvars 
+tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigTyVars use_skols skol_info tyvars 
+  | use_skols
+  = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
+
+  | otherwise
   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
@@ -352,7 +359,8 @@ data LookupTyVarResult      -- The result of a lookupTcTyVar call
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 
-  = case details of
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+    case details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref
                         ; case meta_details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref
                         ; case meta_details of
@@ -414,7 +422,7 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
+zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
                    zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 \end{code}
 
                    zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 \end{code}
 
@@ -442,23 +450,58 @@ zonkTcPredType (ClassP c ts)
 zonkTcPredType (IParam n t)
   = zonkTcType t       `thenM` \ new_t ->
     returnM (IParam n new_t)
 zonkTcPredType (IParam n t)
   = zonkTcType t       `thenM` \ new_t ->
     returnM (IParam n new_t)
+zonkTcPredType (EqPred t1 t2)
+  = zonkTcType t1      `thenM` \ new_t1 ->
+    zonkTcType t2      `thenM` \ new_t2 ->
+    returnM (EqPred new_t1 new_t2)
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
+zonkTopTyVar :: TcTyVar -> TcM TcTyVar
+-- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
+-- to default the kind of ? and ?? etc to *.  This is important to ensure that
+-- instance declarations match.  For example consider
+--     instance Show (a->b)
+--     foo x = show (\_ -> True)
+-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
+-- and that won't match the typeKind (*) in the instance decl.
+--
+-- Because we are at top level, no further constraints are going to affect these
+-- type variables, so it's time to do it by hand.  However we aren't ready
+-- to default them fully to () or whatever, because the type-class defaulting
+-- rules have yet to run.
+
+zonkTopTyVar tv
+  | k `eqKind` default_k = return tv
+  | otherwise
+  = do { tv' <- newFlexiTyVar default_k
+       ; writeMetaTyVar tv (mkTyVarTy tv') 
+       ; return tv' }
+  where
+    k = tyVarKind tv
+    default_k = defaultKind k
+
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
+zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
+
 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
--- When we do this, we also default the kind -- see notes with Kind.defaultKind
+--
+-- The quantified type variables often include meta type variables
+-- we want to freeze them into ordinary type variables, and
+-- default their kind (e.g. from OpenTypeKind to TypeKind)
+--                     -- see notes with Kind.defaultKind
 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | isSkolemTyVar tv = return tv
+  | ASSERT( isTcTyVar tv ) 
+    isSkolemTyVar tv = return tv
        -- It might be a skolem type variable, 
        -- for example from a user type signature
 
        -- It might be a skolem type variable, 
        -- for example from a user type signature
 
@@ -566,10 +609,13 @@ zonkType unbound_var_fn ty
                             go ty              `thenM` \ ty' ->
                             returnM (ForAllTy tyvar ty')
 
                             go ty              `thenM` \ ty' ->
                             returnM (ForAllTy tyvar ty')
 
-    go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
-                            returnM (ClassP c tys')
-    go_pred (IParam n ty)  = go ty             `thenM` \ ty' ->
-                            returnM (IParam n ty')
+    go_pred (ClassP c tys)   = mappM go tys    `thenM` \ tys' ->
+                              returnM (ClassP c tys')
+    go_pred (IParam n ty)    = go ty           `thenM` \ ty' ->
+                              returnM (IParam n ty')
+    go_pred (EqPred ty1 ty2) = go ty1          `thenM` \ ty1' ->
+                              go ty2           `thenM` \ ty2' ->
+                              returnM (EqPred ty1' ty2')
 
 zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
              -> TcTyVar -> TcM TcType
 
 zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
              -> TcTyVar -> TcM TcType
@@ -593,35 +639,20 @@ zonk_tc_tyvar unbound_var_fn tyvar
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-readKindVar  :: KindVar -> TcM (Maybe TcKind)
+readKindVar  :: KindVar -> TcM (MetaDetails)
 writeKindVar :: KindVar -> TcKind -> TcM ()
 readKindVar  kv = readMutVar (kindVarRef kv)
 writeKindVar :: KindVar -> TcKind -> TcM ()
 readKindVar  kv = readMutVar (kindVarRef kv)
-writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
-zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
-                               ; k2' <- zonkTcKind k2
-                               ; returnM (FunKind k1' k2') }
-zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
-                              ; case mb_kind of
-                                   Nothing -> returnM k
-                                   Just k  -> zonkTcKind k }
-zonkTcKind other_kind = returnM other_kind
+zonkTcKind k = zonkTcType k
 
 -------------
 zonkTcKindToKind :: TcKind -> TcM Kind
 
 -------------
 zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
-                                     ; k2' <- zonkTcKindToKind k2
-                                     ; returnM (FunKind k1' k2') }
-
-zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
-                                  ; case mb_kind of
-                                      Nothing -> return liftedTypeKind
-                                      Just k  -> zonkTcKindToKind k }
-
-zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
-zonkTcKindToKind other_kind   = returnM other_kind
+-- When zonking a TcKind to a kind, we need to instantiate kind variables,
+-- Haskell specifies that * is to be used, so we follow that.
+zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
 \end{code}
                        
 %************************************************************************
 \end{code}
                        
 %************************************************************************
@@ -663,9 +694,13 @@ checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
   = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
   = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
-    doptM Opt_GlasgowExts      `thenM` \ gla_exts ->
+    doptM Opt_UnboxedTuples `thenM` \ unboxed ->
+    doptM Opt_Rank2Types       `thenM` \ rank2 ->
+    doptM Opt_RankNTypes       `thenM` \ rankn ->
+    doptM Opt_PolymorphicComponents    `thenM` \ polycomp ->
     let 
     let 
-       rank | gla_exts = Arbitrary
+       rank | rankn = Arbitrary
+            | rank2 = Rank 2
             | otherwise
             = case ctxt of     -- Haskell 98
                 GenPatCtxt     -> Rank 0
             | otherwise
             = case ctxt of     -- Haskell 98
                 GenPatCtxt     -> Rank 0
@@ -676,30 +711,28 @@ checkValidType ctxt ty
                 TySynCtxt _    -> Rank 0
                 ExprSigCtxt    -> Rank 1
                 FunSigCtxt _   -> Rank 1
                 TySynCtxt _    -> Rank 0
                 ExprSigCtxt    -> Rank 1
                 FunSigCtxt _   -> Rank 1
-                ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
-                                               -- constructor, hence rank 1
+                ConArgCtxt _   -> if polycomp
+                           then Rank 2
+                                -- We are given the type of the entire
+                                -- constructor, hence rank 1
+                           else Rank 1
                 ForSigCtxt _   -> Rank 1
                 ForSigCtxt _   -> Rank 1
-                RuleSigCtxt _  -> Rank 1
                 SpecInstCtxt   -> Rank 1
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
                 SpecInstCtxt   -> Rank 1
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
-                       ResSigCtxt   -> isOpenTypeKind   actual_kind
-                       ExprSigCtxt  -> isOpenTypeKind   actual_kind
+                       ResSigCtxt   -> isSubOpenTypeKind        actual_kind
+                       ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       other        -> isArgTypeKind    actual_kind
+                       other        -> isSubArgTypeKind    actual_kind
        
        
-       ubx_tup | not gla_exts = UT_NotOk
-               | otherwise    = case ctxt of
-                                  TySynCtxt _ -> UT_Ok
-                                  ExprSigCtxt -> UT_Ok
-                                  other       -> UT_NotOk
-               -- Unboxed tuples ok in function results,
-               -- but for type synonyms we allow them even at
-               -- top level
+       ubx_tup = case ctxt of
+                     TySynCtxt _ | unboxed -> UT_Ok
+                     ExprSigCtxt | unboxed -> UT_Ok
+                     _                     -> UT_NotOk
     in
        -- Check that the thing has kind Type, and is lifted if necessary
     checkTc kind_ok (kindErr actual_kind)      `thenM_`
     in
        -- Check that the thing has kind Type, and is lifted if necessary
     checkTc kind_ok (kindErr actual_kind)      `thenM_`
@@ -776,7 +809,7 @@ check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty
 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 -- are handled, but the quick thing is just to permit PredTys here.
 check_tau_type rank ubx_tup (PredTy sty) = getDOpts            `thenM` \ dflags ->
 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 -- are handled, but the quick thing is just to permit PredTys here.
 check_tau_type rank ubx_tup (PredTy sty) = getDOpts            `thenM` \ dflags ->
-                                          check_source_ty dflags TypeCtxt sty
+                                          check_pred_ty dflags TypeCtxt sty
 
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
@@ -796,12 +829,14 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
                --      type Foo a = Tree [a]
                --      f :: Foo a b -> ...
        ; case tcView ty of
                --      type Foo a = Tree [a]
                --      f :: Foo a b -> ...
        ; case tcView ty of
-            Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
-            Nothing  -> failWithTc arity_msg
-
-       ; gla_exts <- doptM Opt_GlasgowExts
-       ; if gla_exts then
-       -- If -fglasgow-exts then don't check the type arguments
+            Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
+            Nothing -> unless (isOpenTyCon tc           -- No expansion if open
+                               && tyConArity tc <= length tys) $
+                         failWithTc arity_msg
+
+       ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms
+       ; if ok && not (isOpenTyCon tc) then
+       -- Don't check the type arguments of *closed* synonyms.
        -- This allows us to instantiate a synonym defn with a 
        -- for-all type, or with a partially-applied type synonym.
        --      e.g.   type T a b = a
        -- This allows us to instantiate a synonym defn with a 
        -- for-all type, or with a partially-applied type synonym.
        --      e.g.   type T a b = a
@@ -818,8 +853,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
        }
     
   | isUnboxedTupleTyCon tc
        }
     
   | isUnboxedTupleTyCon tc
-  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
-    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
+  = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed ->
+    checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_`
     mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
                -- Args are allowed to be unlifted, or
                -- more unboxed tuples, so can't use check_arg_ty
     mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
                -- Args are allowed to be unlifted, or
                -- more unboxed tuples, so can't use check_arg_ty
@@ -828,7 +863,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   = mappM_ check_arg_type tys
 
   where
   = mappM_ check_arg_type tys
 
   where
-    ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+    ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
 
     n_args    = length tys
     tc_arity  = tyConArity tc
 
     n_args    = length tys
     tc_arity  = tyConArity tc
@@ -888,31 +923,44 @@ check_valid_theta ctxt []
 check_valid_theta ctxt theta
   = getDOpts                                   `thenM` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
 check_valid_theta ctxt theta
   = getDOpts                                   `thenM` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
-    mappM_ (check_source_ty dflags ctxt) theta
+    mappM_ (check_pred_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
-check_source_ty dflags ctxt pred@(ClassP cls tys)
-  =    -- Class predicates are valid in all contexts
-    checkTc (arity == n_tys) arity_err         `thenM_`
-
-       -- Check the form of the argument types
-    mappM_ check_arg_type tys                          `thenM_`
-    checkTc (check_class_pred_tys dflags ctxt tys)
-           (predTyVarErr pred $$ how_to_allow)
-
+check_pred_ty dflags ctxt pred@(ClassP cls tys)
+  = do {       -- Class predicates are valid in all contexts
+       ; checkTc (arity == n_tys) arity_err
+
+               -- Check the form of the argument types
+       ; mappM_ check_arg_type tys
+       ; checkTc (check_class_pred_tys dflags ctxt tys)
+                (predTyVarErr pred $$ how_to_allow)
+       }
   where
     class_name = className cls
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
   where
     class_name = className cls
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
-    how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
-
-check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-       -- Implicit parameters only allows in type
+    how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
+
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+  = do {       -- Equational constraints are valid in all contexts if type
+               -- families are permitted
+       ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+
+               -- Check the form of the argument types
+       ; check_eq_arg_type ty1
+       ; check_eq_arg_type ty2
+       }
+  where 
+    check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
+
+check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+       -- Implicit parameters only allowed in type
        -- signatures; not in instance decls, superclasses etc
        -- signatures; not in instance decls, superclasses etc
-       -- The reason for not allowing implicit params in instances is a bit subtle
+       -- The reason for not allowing implicit params in instances is a bit
+       -- subtle.
        -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
        -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
        -- discharge all the potential usas of the ?x in e.   For example, a
        -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
        -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
        -- discharge all the potential usas of the ?x in e.   For example, a
@@ -920,18 +968,18 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
-check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
 
 -------------------------
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 
 -------------------------
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
-       InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
+       InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
                                -- Further checks on head and theta in
                                -- checkInstTermination
                                -- Further checks on head and theta in
                                -- checkInstTermination
-       other         -> gla_exts || all tyvar_head tys
+       other         -> flexible_contexts || all tyvar_head tys
   where
   where
-    gla_exts       = dopt Opt_GlasgowExts dflags
+    flexible_contexts = dopt Opt_FlexibleContexts dflags
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 
 -------------------------
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 
 -------------------------
@@ -1005,7 +1053,8 @@ even in a scope where b is in scope.
 
 \begin{code}
 checkFreeness forall_tyvars theta
 
 \begin{code}
 checkFreeness forall_tyvars theta
-  = mappM_ complain (filter is_free theta)
+  = do { flexible_contexts <- doptM Opt_FlexibleContexts
+       ; unless flexible_contexts $ mappM_ complain (filter is_free theta) }
   where    
     is_free pred     =  not (isIPPred pred)
                     && not (any bound_var (varSetElems (tyVarsOfPred pred)))
   where    
     is_free pred     =  not (isIPPred pred)
                     && not (any bound_var (varSetElems (tyVarsOfPred pred)))
@@ -1024,7 +1073,10 @@ checkThetaCtxt ctxt theta
   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+                  $$
+                  parens (ptext SLIT("Use -ftype-families to permit this"))
 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
                          nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
                          nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
@@ -1074,19 +1126,30 @@ checkValidInstHead ty   -- Should be a source type
 
 check_inst_head dflags clas tys
        -- If GlasgowExts then check at least one isn't a type variable
 
 check_inst_head dflags clas tys
        -- If GlasgowExts then check at least one isn't a type variable
-  | dopt Opt_GlasgowExts dflags
-  = mapM_ check_one tys
-
-       -- WITH HASKELL 98, MUST HAVE C (T a b c)
-  | otherwise
-  = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
-           (instTypeErr (pprClassPred clas tys) head_shape_msg)
-
+  = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
+                all tcInstHeadTyNotSynonym tys)
+               (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+       checkTc (dopt Opt_FlexibleInstances dflags ||
+                all tcInstHeadTyAppAllTyVars tys)
+               (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+       checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+                isSingleton tys)
+               (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+       mapM_ check_one tys
   where
   where
-    (first_ty : _) = tys
+    head_type_synonym_msg = parens (
+                text "All instance types must be of the form (T t1 ... tn)" $$
+                text "where T is not a synonym." $$
+                text "Use -XTypeSynonymInstances if you want to disable this.")
 
 
-    head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
-                            text "where T is not a synonym, and a,b,c are distinct type variables")
+    head_type_args_tyvars_msg = parens (
+                text "All instance types must be of the form (T a1 ... an)" $$
+                text "where a1 ... an are distinct type *variables*" $$
+                text "Use -XFlexibleInstances if you want to disable this.")
+
+    head_one_type_msg = parens (
+                text "Only one type can be given in an instance head." $$
+                text "Use -XMultiParamTypeClasses if you want to allow more.")
 
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
 
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
@@ -1112,26 +1175,31 @@ instTypeErr pp_ty msg
 \begin{code}
 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
 checkValidInstance tyvars theta clas inst_tys
 \begin{code}
 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
 checkValidInstance tyvars theta clas inst_tys
-  = do { gla_exts <- doptM Opt_GlasgowExts
-       ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
+  = do { undecidable_ok <- doptM Opt_AllowUndecidableInstances
 
        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
 
        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
-       -- For Haskell 98, checkValidTheta has already done that
-       ; when (gla_exts && not undecidable_ok) $
-              checkInstTermination theta inst_tys
+       -- For Haskell 98 this will already have been done by checkValidTheta,
+    -- but as we may be using other extensions we need to check.
+       ; unless undecidable_ok $
+         mapM_ addErrTc (checkInstTermination inst_tys theta)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
        }
   where
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
        }
   where
-    msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
+    msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+                        undecidableMsg])
 \end{code}
 
 \end{code}
 
-Termination test: each assertion in the context satisfies
+Termination test: the so-called "Paterson conditions" (see Section 5 of
+"Understanding functionsl dependencies via Constraint Handling Rules, 
+JFP Jan 2007).
+
+We check that each assertion in the context satisfies:
  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
@@ -1145,20 +1213,19 @@ The underlying idea is that
 
 
 \begin{code}
 
 
 \begin{code}
-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
-  = do { mappM_ (check_nomore (fvTypes tys))    theta
-       ; mappM_ (check_smaller (sizeTypes tys)) theta }
-
-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
-  = checkTc (null (fvPred pred \\ fvs))
-           (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
-
-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
-  = checkTc (sizePred pred < n)
-           (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+checkInstTermination :: [TcType] -> ThetaType -> [Message]
+checkInstTermination tys theta
+  = mapCatMaybes check theta
+  where
+   fvs  = fvTypes tys
+   size = sizeTypes tys
+   check pred 
+      | not (null (fvPred pred \\ fvs)) 
+      = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+      | sizePred pred >= size
+      = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+      | otherwise
+      = Nothing
 
 predUndecErr pred msg = sep [msg,
                        nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 
 predUndecErr pred msg = sep [msg,
                        nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
@@ -1184,6 +1251,7 @@ fvTypes tys                = concat (map fvType tys)
 fvPred :: PredType -> [TyVar]
 fvPred (ClassP _ tys')     = fvTypes tys'
 fvPred (IParam _ ty)       = fvType ty
 fvPred :: PredType -> [TyVar]
 fvPred (ClassP _ tys')     = fvTypes tys'
 fvPred (IParam _ ty)       = fvType ty
+fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
 
 -- Size of a type: the number of variables and constructors
 sizeType :: Type -> Int
 
 -- Size of a type: the number of variables and constructors
 sizeType :: Type -> Int
@@ -1202,4 +1270,5 @@ sizeTypes xs               = sum (map sizeType xs)
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
 sizePred (IParam _ ty)     = sizeType ty
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
 sizePred (IParam _ ty)     = sizeType ty
+sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
 \end{code}
 \end{code}
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)