Ticky is an RTS-only way; also fix collateral damage to other ways

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

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index de9c341..4a5b2cc 100644 (file)
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -962,17 +962,23 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
                        -- Get location from monad, not from tvs1
             ; let tys      = mkTyVarTys tvs
                   in_scope = mkInScopeSet (mkVarSet tvs)
-                  subst1   = mkTvSubst in_scope (zipTyEnv tvs1 tys)
-                  subst2   = mkTvSubst in_scope (zipTyEnv tvs2 tys)
-                  (theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
-                  (theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
+                  phi1   = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+                  phi2   = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
+                  (theta1,tau1) = tcSplitPhiTy phi1
+                  (theta2,tau2) = tcSplitPhiTy phi2
 
-            ; checkM (equalLength theta1 theta2)
+            ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
+            { checkM (equalLength theta1 theta2)
                      (unifyMisMatch outer False orig_ty1 orig_ty2)
             
             ; uPreds False nb1 theta1 nb2 theta2
             ; uTys nb1 tau1 nb2 tau2
 
+               -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
+            ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
+            ; ifM (any (`elemVarSet` free_tvs) tvs)
+                  (bleatEscapedTvs free_tvs tvs tvs)
+
                -- If both sides are inside a box, we are in a "box-meets-box"
                -- situation, and we should not have a polytype at all.  
                -- If we get here we have two boxes, already filled with
@@ -980,7 +986,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
                -- This check comes last, because the error message is 
                -- extremely unhelpful.  
             ; ifM (nb1 && nb2) (notMonoType ty1)
-            }
+            }}
       where
        (tvs1, body1) = tcSplitForAllTys ty1
        (tvs2, body2) = tcSplitForAllTys ty2
@@ -1366,7 +1372,11 @@ checkTauTvUpdate orig_tv orig_ty
             ; case mb_tys' of
                Just tys' -> return (TyConApp tc tys')
                                -- Retain the synonym (the common case)
-               Nothing   -> go (expectJust "checkTauTvUpdate" 
+               Nothing | isOpenTyCon tc
+                         -> notMonoArgs (TyConApp tc tys)
+                               -- Synonym families must have monotype args
+                       | otherwise
+                         -> go (expectJust "checkTauTvUpdate" 
                                        (tcView (TyConApp tc tys)))
                                -- Try again, expanding the synonym
             }
@@ -1533,6 +1543,16 @@ addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
        <+> ptext SLIT("arguments")
 
 ------------------
+unifyForAllCtxt tvs phi1 phi2 env
+  = returnM (env2, msg)
+  where
+    (env', tvs') = tidyOpenTyVars env tvs      -- NB: not tidyTyVarBndrs
+    (env1, phi1') = tidyOpenType env' phi1
+    (env2, phi2') = tidyOpenType env1 phi2
+    msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
+               ptext SLIT("          and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
+
+------------------
 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
        -- tv1 and ty2 are zonked already
   = returnM msg
@@ -1588,6 +1608,13 @@ notMonoType ty
              msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
        ; failWithTcM (env1, msg) }
 
+notMonoArgs ty
+  = do { ty' <- zonkTcType ty
+       ; env0 <- tcInitTidyEnv
+       ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+             msg = ptext SLIT("Arguments of synonym family must be monotypes") <+> quotes (ppr tidy_ty)
+       ; failWithTcM (env1, msg) }
+
 occurCheck tyvar ty
   = do { env0 <- tcInitTidyEnv
        ; ty'  <- zonkTcType ty