-XImpredicativeTypes implies -XRankNTypes, and improve error msg in TcMType

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

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 1addfe4..75ce6c9 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -524,6 +524,7 @@ writeMetaTyVar tyvar ty
     -- 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 )
+       ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty)
        ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
   where
     _k1 = tyVarKind tyvar
@@ -762,8 +763,11 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | ASSERT( isTcTyVar tv ) 
-    isSkolemTyVar tv = return tv
+  | ASSERT2( isTcTyVar tv, ppr tv ) 
+    isSkolemTyVar tv 
+  = do { kind <- zonkTcType (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
        -- It might be a skolem type variable, 
        -- for example from a user type signature
 
@@ -895,12 +899,14 @@ zonkType unbound_var_fn ty
 
        -- The two interesting cases!
     go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
-                      | otherwise       = return (TyVarTy tyvar)
+                      | otherwise       = liftM TyVarTy $ 
+                                             zonkTyVar unbound_var_fn tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
 
     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
                              ty' <- go ty
-                             return (ForAllTy tyvar ty')
+                             tyvar' <- zonkTyVar unbound_var_fn tyvar
+                             return (ForAllTy tyvar' ty')
 
     go_pred (ClassP c tys)   = do tys' <- mapM go tys
                                   return (ClassP c tys')
@@ -910,7 +916,7 @@ zonkType unbound_var_fn ty
                                   ty2' <- go ty2
                                   return (EqPred ty1' ty2')
 
-zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
+zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
              -> TcTyVar -> TcM TcType
 zonk_tc_tyvar unbound_var_fn tyvar 
   | not (isMetaTyVar tyvar)    -- Skolems
@@ -921,6 +927,18 @@ zonk_tc_tyvar unbound_var_fn tyvar
        ; case cts of
            Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
            Indirect ty -> zonkType unbound_var_fn ty  }
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their
+-- kind contains types).
+--
+zonkTyVar :: (TcTyVar -> TcM Type)      -- What to do for an unbound mutable var
+         -> TyVar -> TcM TyVar
+zonkTyVar unbound_var_fn tv 
+  | isCoVar tv
+  = do { kind <- zonkType unbound_var_fn (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
+  | otherwise = return tv
 \end{code}
 
 
@@ -997,18 +1015,22 @@ checkValidType ctxt ty = do
                   | otherwise = Rank n
        rank
          = case ctxt of
-                GenPatCtxt     -> MustBeMonoType
                 DefaultDeclCtxt-> MustBeMonoType
                 ResSigCtxt     -> MustBeMonoType
                 LamPatSigCtxt  -> gen_rank 0
                 BindPatSigCtxt -> gen_rank 0
                 TySynCtxt _    -> gen_rank 0
+                GenPatCtxt     -> gen_rank 1
+                       -- This one is a bit of a hack
+                       -- See the forall-wrapping in TcClassDcl.mkGenericInstance              
+
                 ExprSigCtxt    -> gen_rank 1
                 FunSigCtxt _   -> gen_rank 1
                 ConArgCtxt _   | polycomp -> gen_rank 2
                                 -- We are given the type of the entire
                                 -- constructor, hence rank 1
                                | otherwise -> gen_rank 1
+
                 ForSigCtxt _   -> gen_rank 1
                 SpecInstCtxt   -> gen_rank 1
 
@@ -1044,6 +1066,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
@@ -1117,7 +1140,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   
@@ -1194,6 +1217,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
@@ -1300,6 +1324,14 @@ 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 -XFlexibleContexts to permit this"))
 
+check_pred_ty _ (ClassSCCtxt _) (EqPred _ _)
+  =   -- We do not yet support superclass equalities.
+    failWithTc $
+      sep [ ptext (sLit "The current implementation of type families does not")
+          , ptext (sLit "support equality constraints in superclass contexts.")
+          , ptext (sLit "They are planned for a future release.")
+          ]
+
 check_pred_ty dflags _ pred@(EqPred ty1 ty2)
   = do {       -- Equational constraints are valid in all contexts if type
                -- families are permitted