X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=7ac2677e5b7b9f7ed6a49760d660ebaf6e5c84e5;hb=edf6bdfb5dee21f9bc5077083e5350ee64efffbc;hp=a2dae5e1d37c13f137972b548b08a10efdb7302f;hpb=9fe510d19e48f1cefdf3591c8669cd74a63867b7;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index a2dae5e..7ac2677 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -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
@@ -655,6 +651,7 @@ This might not necessarily show up in kind checking.
 \begin{code}
 data UserTypeCtxt 
   = FunSigCtxt Name	-- Function type signature
+			-- Also used for types in SPECIALISE pragmas
   | ExprSigCtxt		-- Expression type signature
   | ConArgCtxt Name	-- Data constructor argument
   | TySynCtxt Name	-- RHS of a type synonym decl
@@ -667,6 +664,7 @@ data UserTypeCtxt
   | ForSigCtxt Name	-- Foreign inport or export signature
   | RuleSigCtxt Name 	-- Signature on a forall'd variable in a RULE
   | DefaultDeclCtxt	-- Types in a default declaration
+  | SpecInstCtxt	-- SPECIALISE instance pragma
 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []
@@ -693,6 +691,7 @@ pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature
 pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
 pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty SpecInstCtxt    = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]
 
 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 \end{code}
@@ -718,6 +717,7 @@ checkValidType ctxt ty
 						-- constructor, hence rank 1
 		 ForSigCtxt _	-> Rank 1
 		 RuleSigCtxt _	-> Rank 1
+		 SpecInstCtxt   -> Rank 1
 
 	actual_kind = typeKind ty
 
@@ -727,7 +727,7 @@ checkValidType ctxt ty
 			ExprSigCtxt  -> isOpenTypeKind 	 actual_kind
 			GenPatCtxt   -> isLiftedTypeKind actual_kind
 			ForSigCtxt _ -> isLiftedTypeKind actual_kind
-			other	     -> isArgTypeKind       actual_kind
+			other	     -> isArgTypeKind    actual_kind
 	
 	ubx_tup | not gla_exts = UT_NotOk
 		| otherwise    = case ctxt of
@@ -821,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
 
@@ -852,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 ->
@@ -868,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
 
@@ -979,15 +974,20 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 -------------------------
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
+	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
@@ -1078,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