Store a SrcSpan instead of a SrcLoc inside a Name

[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 4a12536..6e72536 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -47,7 +47,8 @@ module TcMType (
   --------------------------------
   -- Zonking
   zonkType, zonkTcPredType, 
   --------------------------------
   -- Zonking
   zonkType, zonkTcPredType, 

-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkQuantifiedTyVar, zonkQuantifiedTyVars,

   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
 
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
 

@@ -61,7 +62,6 @@ module TcMType (
 import TypeRep
 import TcType
 import Type
 import TypeRep
 import TcType
 import Type

-import Type

 import Coercion
 import Class
 import TyCon
 import Coercion
 import Class
 import TyCon

@@ -81,7 +81,7 @@ import UniqSupply
 import SrcLoc
 import Outputable
 
 import SrcLoc
 import Outputable
 

-import Control.Monad   ( when )
+import Control.Monad   ( when, unless )

 import Data.List       ( (\\) )
 \end{code}
 
 import Data.List       ( (\\) )
 \end{code}
 

@@ -161,7 +161,7 @@ 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 ]
 

-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcLoc -> TyVar -> TcM TcTyVar
+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,
 -- Instantiate the tyvar, using 
 --     * the occ-name and kind of the supplied tyvar, 
 --     * the unique from the monad,

@@ -171,7 +171,7 @@ tcInstSkolTyVar info mb_loc tyvar
   = do { uniq <- newUnique
        ; let old_name = tyVarName tyvar
              kind     = tyVarKind tyvar
   = do { uniq <- newUnique
        ; let old_name = tyVarName tyvar
              kind     = tyVarKind tyvar

-             loc      = mb_loc `orElse` getSrcLoc old_name
+             loc      = mb_loc `orElse` getSrcSpan old_name

              new_name = mkInternalName uniq (nameOccName old_name) loc
        ; return (mkSkolTyVar new_name kind info) }
 
              new_name = mkInternalName uniq (nameOccName old_name) loc
        ; return (mkSkolTyVar new_name kind info) }
 

@@ -179,7 +179,7 @@ tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 -- Get the location from the monad
 tcInstSkolTyVars info tyvars 
   = do         { span <- getSrcSpanM
 -- Get the location from the monad
 tcInstSkolTyVars info tyvars 
   = do         { span <- getSrcSpanM

-       ; mapM (tcInstSkolTyVar info (Just (srcSpanStart span))) tyvars }
+       ; mapM (tcInstSkolTyVar info (Just span)) tyvars }

 
 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 
 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants

@@ -359,7 +359,7 @@ data LookupTyVarResult      -- The result of a lookupTcTyVar call
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 lookupTcTyVar tyvar 

-  = ASSERT( isTcTyVar tyvar )
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )

     case details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref
     case details of
       SkolemTv _   -> return (DoneTv details)
       MetaTv _ ref -> do { meta_details <- readMutVar ref

@@ -422,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}
 

@@ -484,17 +484,24 @@ zonkTopTyVar tv
     k = tyVarKind tv
     default_k = defaultKind k
 
     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
 

@@ -819,12 +826,15 @@ 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
+            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

 
        ; gla_exts <- doptM Opt_GlasgowExts
 
        ; gla_exts <- doptM Opt_GlasgowExts

-       ; if gla_exts then
-       -- If -fglasgow-exts then don't check the type arguments
+       ; if gla_exts && not (isOpenTyCon tc) then
+       -- If -fglasgow-exts 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

@@ -917,14 +927,14 @@ check_valid_theta ctxt theta
 
 -------------------------
 check_pred_ty dflags ctxt pred@(ClassP cls tys)
 
 -------------------------
 check_pred_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)
-
+  = 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
   where
     class_name = className cls
     arity      = classArity cls

@@ -932,10 +942,23 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     arity_err  = arityErr "Class" class_name arity n_tys
     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 
     arity_err  = arityErr "Class" class_name arity n_tys
     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 

+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+  = do {       -- Equational constraints are valid in all contexts if indexed
+               -- types are permitted
+       ; checkTc (dopt Opt_IndexedTypes 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
 check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty

-       -- Implicit parameters only allows in type
+       -- 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

@@ -1050,6 +1073,9 @@ checkThetaCtxt ctxt theta
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty

+eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+                  $$
+                  parens (ptext SLIT("Use -findexed-types 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)

@@ -1110,8 +1136,8 @@ check_inst_head dflags clas tys
   where
     (first_ty : _) = tys
 
   where
     (first_ty : _) = tys
 

-    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_shape_msg = parens (text "The instance type must be of form (T a1 ... an)" $$
+                            text "where T is not a synonym, and a1 ... an are distinct type *variables*")

 
        -- 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.  

@@ -1146,7 +1172,7 @@ checkValidInstance tyvars theta clas 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) $
        -- Check that instance inference will terminate (if we care)
        -- For Haskell 98, checkValidTheta has already done that
        ; when (gla_exts && not undecidable_ok) $

-         mapM_ failWithTc (checkInstTermination inst_tys theta)
+         mapM_ addErrTc (checkInstTermination inst_tys theta)

        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)

@@ -1157,7 +1183,11 @@ checkValidInstance tyvars theta clas inst_tys
                         undecidableMsg])
 \end{code}
 
                         undecidableMsg])
 \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.