Equality constraint solver is now externally pure

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

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 6de3dd2..525ba0d 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -35,16 +35,17 @@ module TcMType (
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
   tcInstSigType,
   tcInstSkolTyVars, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
+  tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds,
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, checkValidInstance, 
-  checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
+  checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds,
   checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
   unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
+  growPredTyVars, growTyVars, growThetaTyVars,
 
   --------------------------------
   -- Zonking
@@ -77,6 +78,7 @@ import VarSet
 import ErrUtils
 import DynFlags
 import Util
+import Bag
 import Maybes
 import ListSetOps
 import UniqSupply
@@ -336,6 +338,27 @@ Rather, we should bind t to () (= non_var_ty2).
 
 --------------
 
+Execute a bag of type variable bindings.
+
+\begin{code}
+execTcTyVarBinds :: TcTyVarBinds -> TcM ()
+execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList
+  where
+    execTcTyVarBind (TcTyVarBind tv ty)
+      = do { ASSERTM2( do { details <- readMetaTyVar tv
+                          ; return (isFlexi details) }, ppr tv )
+           ; ty' <- if isCoVar tv 
+                    then return ty 
+                    else do { maybe_ty <- checkTauTvUpdate tv ty
+                            ; case maybe_ty of
+                                Nothing -> pprPanic "TcRnMonad.execTcTyBind"
+                                             (ppr tv <+> text ":=" <+> ppr ty)
+                                Just ty' -> return ty'
+                            }
+           ; writeMetaTyVar tv ty'
+           }
+\end{code}
+
 Error mesages in case of kind mismatch.
 
 \begin{code}
@@ -521,14 +544,17 @@ writeMetaTyVar tyvar ty
     return ()
   | otherwise
   = ASSERT( isMetaTyVar tyvar )
-    -- TOM: It should also work for coercions
-    -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
-    do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
+    ASSERT2( isCoVar tyvar || typeKind ty `isSubKind` tyVarKind tyvar, 
+             (ppr tyvar <+> ppr (tyVarKind tyvar)) 
+             $$ (ppr ty <+> ppr (typeKind ty)) )
+    do { if debugIsOn then do { details <- readMetaTyVar tyvar; 
+-- FIXME                              ; ASSERT2( not (isFlexi details), ppr tyvar )
+                              ; WARN( not (isFlexi details), ppr tyvar )
+                                return () }
+                       else return () 
+
        ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty)
        ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
-  where
-    _k1 = tyVarKind tyvar
-    _k2 = typeKind ty
 \end{code}
 
 
@@ -1066,6 +1092,7 @@ checkValidMonoType ty = check_mono_type MustBeMonoType ty
 data Rank = ArbitraryRank        -- Any rank ok
           | MustBeMonoType       -- Monotype regardless of flags
          | TyConArgMonoType      -- Monotype but could be poly if -XImpredicativeTypes
+         | SynArgMonoType        -- Monotype but could be poly if -XLiberalTypeSynonyms
           | Rank Int             -- Rank n, but could be more with -XRankNTypes
 
 decRank :: Rank -> Rank                  -- Function arguments
@@ -1139,7 +1166,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
        ; liberal <- doptM Opt_LiberalTypeSynonyms
        ; if not liberal || isOpenSynTyCon tc then
                -- For H98 and synonym families, do check the type args
-               mapM_ (check_mono_type TyConArgMonoType) tys
+               mapM_ (check_mono_type SynArgMonoType) tys
 
          else  -- In the liberal case (only for closed syns), expand then check
          case tcView ty of   
@@ -1216,6 +1243,7 @@ forAllTyErr rank ty
     suggestion = case rank of
                   Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
                   TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+                  SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
                   _ -> empty      -- Polytype is always illegal
 
 unliftedArgErr, ubxArgTyErr :: Type -> SDoc
@@ -1414,7 +1442,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars
   = mapM_ complain (filter is_ambig theta)
   where
     complain pred     = addErrTc (ambigErr pred)
-    extended_tau_vars = grow theta tau_tyvars
+    extended_tau_vars = growThetaTyVars theta tau_tyvars
 
        -- See Note [Implicit parameters and ambiguity] in TcSimplify
     is_ambig pred     = isClassPred  pred &&
@@ -1428,6 +1456,28 @@ ambigErr pred
   = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
         nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
                 ptext (sLit "must be reachable from the type after the '=>'"))]
+
+--------------------------
+-- For this 'grow' stuff see Note [Growing the tau-tvs using constraints] in Inst
+
+growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
+-- Finds a fixpoint
+growThetaTyVars theta tvs
+  | null theta = tvs
+  | otherwise  = fixVarSet mk_next tvs
+  where
+    mk_next tvs = foldr growPredTyVars tvs theta
+
+
+growPredTyVars :: TcPredType -> TyVarSet -> TyVarSet
+-- Here is where the special case for inplicit parameters happens
+growPredTyVars (IParam _ ty) tvs = tvs `unionVarSet` tyVarsOfType ty
+growPredTyVars pred          tvs = growTyVars (tyVarsOfPred pred) tvs
+
+growTyVars :: TyVarSet -> TyVarSet -> TyVarSet
+growTyVars new_tvs tvs 
+  | new_tvs `intersectsVarSet` tvs = tvs `unionVarSet` new_tvs
+  | otherwise                     = tvs
 \end{code}
     
 In addition, GHC insists that at least one type variable