X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=fa129d3927fd04c2a6beb0372160927c648cca42;hb=3d8ae1e7ba9f238959ca5395b17c485eda5d70e9;hp=3a232b772bbbc7cd9080894e2c54b6a50cd15a5b;hpb=59c9c122f942f348008d4ed8ba088286343d63d3;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index 3a232b7..fa129d3 100644
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -34,6 +34,7 @@ module TcMType (
   Rank, UserTypeCtxt(..), checkValidType, 
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, checkValidInstance, checkAmbiguity,
+  checkInstTermination,
   arityErr, 
 
   --------------------------------
@@ -89,14 +90,15 @@ import Kind		( isSubKind )
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
-import FunDeps		( grow, checkInstFDs )
+import FunDeps		( grow, checkInstCoverage )
 import Name		( Name, setNameUnique, mkSysTvName )
 import VarSet
-import DynFlags		( dopt, DynFlag(..), DynFlags )
+import DynFlags		( dopt, DynFlag(..) )
 import Util		( nOfThem, isSingleton, notNull )
 import ListSetOps	( removeDups )
 import Outputable
 
+import Control.Monad	( when )
 import Data.List	( (\\) )
 \end{code}
 
@@ -925,12 +927,13 @@ 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
-	InstThetaCtxt -> gla_exts || all tcIsTyVarTy tys
+	InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
 				-- Further checks on head and theta in
 				-- checkInstTermination
 	other	      -> gla_exts || all tyvar_head tys
   where
-    gla_exts 	   = dopt Opt_GlasgowExts dflags
+    gla_exts       = dopt Opt_GlasgowExts dflags
+    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
 
 -------------------------
 tyvar_head ty			-- Haskell 98 allows predicates of form 
@@ -1023,7 +1026,7 @@ checkThetaCtxt ctxt theta
 	  ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred  = sep [ptext SLIT("Non-type variable argument"),
+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)
 
@@ -1073,24 +1076,27 @@ 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
   | dopt Opt_GlasgowExts dflags
-  = returnM ()
+  = mapM_ check_one tys
 
 	-- WITH HASKELL 98, MUST HAVE C (T a b c)
-  | isSingleton tys,
-    tcValidInstHeadTy first_ty
-  = returnM ()
-
   | otherwise
-  = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
+  = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
+	    (instTypeErr (pprClassPred clas tys) head_shape_msg)
 
   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")
-\end{code}
 
-\begin{code}
+	-- For now, I only allow tau-types (not polytypes) in 
+	-- the head of an instance decl.  
+	-- 	E.g.  instance C (forall a. a->a) is rejected
+	-- One could imagine generalising that, but I'm not sure
+	-- what all the consequences might be
+    check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
+		      ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+
 instTypeErr pp_ty msg
   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
 	 nest 4 msg]
@@ -1107,21 +1113,23 @@ instTypeErr pp_ty msg
 \begin{code}
 checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
 checkValidInstance tyvars theta clas inst_tys
-  = do	{ dflags <- getDOpts
+  = do	{ gla_exts <- doptM Opt_GlasgowExts
+	; undecidable_ok <- doptM Opt_AllowUndecidableInstances
 
 	; checkValidTheta InstThetaCtxt theta
 	; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
-	-- Check that instance inference will termainate
+	-- Check that instance inference will terminate (if we care)
 	-- For Haskell 98, checkValidTheta has already done that
-	; checkInstTermination dflags theta inst_tys
+	; when (gla_exts && not undecidable_ok) $
+	       checkInstTermination theta inst_tys
 	
 	-- The Coverage Condition
-	; checkTc (checkInstFDs theta clas inst_tys)
+	; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
 	  	  (instTypeErr (pprClassPred clas inst_tys) msg)
 	}
   where
-    msg  = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class"))
+    msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
 \end{code}
 
 Termination test: each assertion in the context satisfies
@@ -1129,16 +1137,19 @@ Termination test: each assertion in the context satisfies
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
 This is only needed with -fglasgow-exts, as Haskell 98 restrictions
-(which have already been checked) guarantee termination.
+(which have already been checked) guarantee termination. 
+
+The underlying idea is that 
+
+    for any ground substitution, each assertion in the
+    context has fewer type constructors than the head.
+
 
 \begin{code}
-checkInstTermination :: DynFlags -> ThetaType -> [TcType] -> TcM ()
-checkInstTermination dflags theta tys
-  | not (dopt Opt_GlasgowExts dflags)         = returnM ()
-  | dopt Opt_AllowUndecidableInstances dflags = returnM ()
-  | otherwise = do
-    mappM_ (check_nomore (fvTypes tys)) theta
-    mappM_ (check_smaller (sizeTypes tys)) theta
+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