[project @ 2005-12-16 15:15:08 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 97be0a9..7ac2677 100644 (file)
@@ -47,13 +47,13 @@ module TcMType (
 
 -- friends:
 import HsSyn           ( LHsType )
-import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
+import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
                          ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
                          MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, 
+                         tcCmpPred, tcEqType, isClassPred, 
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcValidInstHeadTy, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, 
@@ -61,9 +61,9 @@ import TcType         ( TcType, TcThetaType, TcTauType, TcPredType,
                          typeKind, isFlexi, isSkolemTyVar,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, 
+                         tyVarsOfType, tyVarsOfTypes, tcView,
                          pprPred, pprTheta, pprClassPred )
-import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind,
                          isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
                          liftedTypeKind, defaultKind
                        )
@@ -83,7 +83,7 @@ import VarEnv
 import DynFlags        ( dopt, DynFlag(..) )
 import UniqSupply      ( uniqsFromSupply )
 import Util            ( nOfThem, isSingleton, notNull )
-import ListSetOps      ( removeDups )
+import ListSetOps      ( removeDups, findDupsEq )
 import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
@@ -527,11 +527,7 @@ zonkType unbound_var_fn rflag ty
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
                                    returnM (TyConApp tycon tys')
 
-    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
-                                   go ty2              `thenM` \ ty2' ->
-                                   returnM (NoteTy (SynNote ty1') ty2')
-
-    go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
+    go (NoteTy _ ty2)            = go ty2      -- Discard free-tyvar annotations
 
     go (PredTy p)                = go_pred p           `thenM` \ p' ->
                                    returnM (PredTy p')
@@ -589,8 +585,8 @@ zonkTyVar unbound_var_fn rflag tyvar
 \begin{code}
 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 writeKindVar :: KindVar -> TcKind -> TcM ()
-readKindVar  (KVar _ ref)     = readMutVar ref
-writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+readKindVar  kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
@@ -825,29 +821,6 @@ check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 check_tau_type rank ubx_tup (AppTy ty1 ty2)
   = check_arg_type ty1 `thenM_` check_arg_type ty2
 
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
-       -- Synonym notes are built only when the synonym is 
-       -- saturated (see Type.mkSynTy)
-  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
-    (if gla_exts then
-       -- If -fglasgow-exts then don't check the 'note' part.
-       -- 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
-       --             type S m   = m ()
-       --             f :: S (T Int)
-       -- Here, T is partially applied, so it's illegal in H98.
-       -- But if you expand S first, then T we get just 
-       --             f :: Int
-       -- which is fine.
-       returnM ()
-    else
-       -- For H98, do check the un-expanded part
-       check_tau_type rank ubx_tup syn         
-    )                                          `thenM_`
-
-    check_tau_type rank ubx_tup ty
-
 check_tau_type rank ubx_tup (NoteTy other_note ty)
   = check_tau_type rank ubx_tup ty
 
@@ -856,8 +829,31 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
        -- synonym application, leaving it to checkValidType (i.e. right here)
        -- to find the error
-    checkTc syn_arity_ok arity_msg     `thenM_`
-    mappM_ check_arg_type tys
+    do {       -- It's OK to have an *over-applied* type synonym
+               --      data Tree a b = ...
+               --      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
+       -- 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
+       --             type S m   = m ()
+       --             f :: S (T Int)
+       -- Here, T is partially applied, so it's illegal in H98.
+       -- But if you expand S first, then T we get just 
+       --             f :: Int
+       -- which is fine.
+               returnM ()
+         else
+               -- For H98, do check the type args
+               mappM_ check_arg_type tys
+       }
     
   | isUnboxedTupleTyCon tc
   = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
@@ -872,11 +868,6 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 
-    syn_arity_ok = tc_arity <= n_args
-               -- It's OK to have an *over-applied* type synonym
-               --      data Tree a b = ...
-               --      type Foo a = Tree [a]
-               --      f :: Foo a b -> ...
     n_args    = length tys
     tc_arity  = tyConArity tc
 
@@ -986,13 +977,17 @@ check_class_pred_tys dflags ctxt tys
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
        InstHeadCtxt  -> True   -- We check for instance-head 
                                -- formation in checkValidInstHead
-       InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
+       InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
        other         -> gla_exts       || all tyvar_head tys
   where
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
     gla_exts      = dopt Opt_GlasgowExts dflags
 
 -------------------------
+distinct_tyvars tys    -- Check that the types are all distinct type variables
+  = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
+
+-------------------------
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable
@@ -1083,7 +1078,8 @@ checkThetaCtxt ctxt theta
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+predTyVarErr pred  = sep [ptext SLIT("Non-type variables, or repeated type variables,"),
+                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 
 arityErr kind name n m