diff --git a/src/Type/InferMonad.hs b/src/Type/InferMonad.hs
index e898e7ee6..34048b13b 100644
--- a/src/Type/InferMonad.hs
+++ b/src/Type/InferMonad.hs
@@ -581,8 +581,8 @@ occursInContext tv extraFree
   Unification errors
 --------------------------------------------------------------------------}
 unifyError :: Context -> Range -> UnifyError -> Type -> Type -> Inf a
-unifyError context range (NoMatchEffect eff1 eff2) _ _
-  = unifyError context range NoMatch eff2 eff1
+unifyError context range (NoMatchEffect eff1 eff2 effectMismatch) _ _
+  = unifyError context range (NoMatch (Just effectMismatch)) eff2 eff1
 unifyError context range err xtp1 xtp2
   = do free <- freeInGamma
        tp1 <- subst xtp1 >>= normalizeX False free
@@ -599,6 +599,7 @@ unifyError' env context range err tp1 tp2
                ,(text ("inferred " ++ nameType), nice2)
                ]
                ++ nomatch
+               ++ effectDiffs
                ++ extra
                ++ hint
               )
@@ -627,10 +628,36 @@ unifyError' env context range err tp1 tp2
          then "effect"
          else "type"
 
+    effectDiffs
+      = case err of
+          NoMatch (Just diff) -> effectDiffs' diff
+          NoMatchEffect _ _ diff -> effectDiffs' diff
+          _ -> []
+
+    effectDiffs' diff = unexpectedMessages ++ missingMessages
+      where
+        niceUnexpected = map (Pretty.niceType env) (unexpectedEffectLabels diff)
+        niceMissing = map (Pretty.niceType env) (missingEffectLabels diff)
+        unexpectedMessages = if null niceUnexpected
+          then []
+          else [(text "unexpected", hsep (punctuate comma niceUnexpected))]
+
+        missingMessages = if null niceMissing
+          then []
+          else [(text "missing",
+            vsep [
+              hsep (punctuate comma niceMissing),
+              hsep [
+                text "Consider using",
+                Pretty.keyword env "mask",
+                text "or adding it to the function's effect type"
+              ]
+            ]
+          )]
 
     (message,hint)
       = case err of
-          NoMatch     -> (nameType ++ "s do not match",[])
+          NoMatch _ -> (nameType ++ "s do not match",[])
           NoMatchKind -> ("kinds do not match",[])
           NoMatchSkolem kind
                       -> ("abstract types do not match",if (not (null extra))
@@ -640,7 +667,7 @@ unifyError' env context range err tp1 tp2
                                                                          else text "an higher-rank type escapes its scope?")])
           NoSubsume   -> ("type is not polymorphic enough",[(text "hint",text "give a higher-rank type annotation to a function parameter?")])
           Infinite    -> ("types do not match (due to an infinite type)",[(text "hint",text "give a type to the function definition?")])
-          NoMatchEffect{}-> ("effects do not match",[])
+          NoMatchEffect _ _ _ -> ("effects do not match",[])
           NoArgMatch n m -> if (m<0)
                              then ("only functions can be applied",[])
                              else ("application has too " ++ (if (n > m) then "few" else "many") ++ " arguments"
diff --git a/src/Type/Unify.hs b/src/Type/Unify.hs
index 559107b9c..c0f5e9328 100644
--- a/src/Type/Unify.hs
+++ b/src/Type/Unify.hs
@@ -18,6 +18,8 @@ module Type.Unify ( Unify, UnifyError(..), runUnify, runUnifyEx
                   , matchArguments
                   , matchShape, pureMatchShape
                   , extractNormalizeEffect
+                  , unexpectedEffectLabels
+                  , missingEffectLabels
                   ) where
 
 import Control.Applicative
@@ -75,7 +77,7 @@ overlaps range free tp1 tp2
                  fo1 = take hi (map snd fixed1 ++ map (unOptional . snd) optional1 ++ map snd implicit1)
                  fo2 = take hi (map snd fixed2 ++ map (unOptional . snd) optional2 ++ map snd implicit2)
              in if (length fo1 /= length fo2)
-                 then unifyError NoMatch  -- one has more fixed arguments than the other can ever get
+                 then unifyError noMatchTypes  -- one has more fixed arguments than the other can ever get
                  else do unifies fo1 fo2
                          return ()
 
@@ -87,10 +89,10 @@ matchNamed matchSome range free tp n {- given args -} named mbExpResTp
   = do rho1 <- instantiate range tp
        case splitFunType rho1 of
          Nothing
-          -> unifyError NoMatch
+          -> unifyError noMatchTypes
          Just (pars,_,resTp)
           -> if (n + length named > length pars)
-              then unifyError NoMatch
+              then unifyError noMatchTypes
               else let npars = drop n pars
                        names = map fst npars
                    in if (all (\name -> name `elem` names) named)
@@ -102,8 +104,8 @@ matchNamed matchSome range free tp n {- given args -} named mbExpResTp
                                let rest = [(nm,tp) | (nm,tp) <- npars, not (nm `elem` named)]
                                if (matchSome || all isOptionalOrImplicit rest)
                                 then subst rho1
-                                else unifyError NoMatch
-                       else unifyError NoMatch
+                                else unifyError noMatchTypes
+                       else unifyError noMatchTypes
 
 
 -- | Does a function type match the given arguments? if the first argument 'matchSome' is true,
@@ -124,7 +126,7 @@ matchArguments matchSome range free tp fixed named mbExpResTp
 
          Just (pars,_,resTp)
           -> if (length fixed + length named > length pars)
-              then unifyError NoMatch
+              then unifyError noMatchTypes
               else do -- trace (" matchArguments: " ++ show (map pretty pars, map pretty fixed, map pretty named)) $ return ()
                       -- subsume fixed parameters
                       let parsNotNamedArg = filter (\(nm,tp) -> nm `notElem` map fst named) pars
@@ -132,7 +134,7 @@ matchArguments matchSome range free tp fixed named mbExpResTp
                       mapM_  (\(tpar,targ) -> subsumeSubst range free (unOptional tpar) targ) (zip (map snd fpars) fixed)
                       -- subsume named parameters
                       mapM_ (\(name,targ) -> case lookup name pars of
-                                               Nothing   -> unifyError NoMatch
+                                               Nothing   -> unifyError noMatchTypes
                                                Just tpar -> subsumeSubst range free (unOptional tpar) targ
                             ) named
                       -- check if the result type matches
@@ -143,7 +145,7 @@ matchArguments matchSome range free tp fixed named mbExpResTp
                       -- check the rest is optional or implicit
                       if (matchSome || all isOptionalOrImplicit rest)
                         then do subst rho1
-                        else unifyError NoMatch
+                        else unifyError noMatchTypes
 
 subsumeSubst :: Range -> Tvs -> Type -> Type -> Unify (Type,Rho, Core.Expr -> Core.Expr)
 subsumeSubst range free tp1 tp2
@@ -160,9 +162,9 @@ matchShape tp1 tp2
        codom <- nub <$>
                 mapM (\(_,t) -> case t of
                                   TVar tv -> return tv
-                                  _       -> unifyError NoMatch) (subList sub)
+                                  _       -> unifyError noMatchTypes) (subList sub)
        let oneToOne = (length dom == length codom)
-       if oneToOne then return () else unifyError NoMatch
+       if oneToOne then return () else unifyError noMatchTypes
 
 pureMatchShape :: Type -> Type -> Bool
 pureMatchShape tp1 tp2
@@ -274,8 +276,9 @@ unify f1@(TFun args1 eff1 res1) f2@(TFun args2 eff2 res2) | length args1 == leng
        withError (effErr seff1 seff2) (unify seff1 seff2)
   where
     -- specialize to sub-part of the type for effect unification errors
-    effErr eff1 eff2 NoMatch              = NoMatchEffect eff1 eff2
-    effErr eff1 eff2 (NoMatchEffect _ _)  = NoMatchEffect eff1 eff2
+    effErr eff1 eff2 (NoMatch diff) = NoMatchEffect eff1 eff2 (maybeEffectMismatch diff)
+
+    effErr eff1 eff2 (NoMatchEffect _ _ diff)  = NoMatchEffect eff1 eff2 diff
     effErr eff1 eff2 err                  = err
 
 -- quantified types
@@ -323,9 +326,19 @@ unify tp1 (TSyn _ _ tp2)
 unify (TVar (TypeVar _ kind Skolem)) (TVar (TypeVar _ _ Skolem))
   = unifyError (NoMatchSkolem kind)
 
+-- expected a skolem, got some other effect type
+unify (TVar (TypeVar _ kind Skolem)) tp2 | isKindEffect kind
+  = -- trace ("no match (left is skolem): " ++ show (pretty tp2)) $
+    unifyError $ NoMatch (Just $ effectMismatchMissing tp2)
+
+-- expected `total`, got tp2
+unify tp1 tp2 | isEffectEmpty tp1
+  = -- trace ("no match (left is total): " ++  show (pretty tp2)) $
+    unifyError $ NoMatch (Just $ effectMismatchUnexpected tp2)
+
 unify tp1 tp2
   = -- trace ("no match: " ++  show (pretty tp1, pretty tp2)) $
-    unifyError NoMatch
+    unifyError noMatchTypes
 
 
 -- | Unify a type variable with a type
@@ -339,7 +352,7 @@ unifyTVar tv@(TypeVar id kind Meta) tp
              _        -> unifyError Infinite
      else case etp of
             TVar (TypeVar _ _ Bound)
-              -> unifyError NoMatch -- can't unify with bound variables
+              -> unifyError noMatchTypes -- can't unify with bound variables
             TVar tv2@(TypeVar id2 _ Meta) | id <= id2
               -> if (id < id2)
                   then unifyTVar tv2 (TVar tv)
@@ -479,11 +492,34 @@ data Res a    = Ok !a !St
               | Err UnifyError !St
 data St       = St{ uniq :: !Int, sub :: !Sub }
 
+data EffectMismatch = EffectMismatch
+  { unexpectedEffectLabels :: [Type]
+  , missingEffectLabels :: [Type]
+  } deriving Show
+
+maybeEffectMismatch (Just diff) = diff
+maybeEffectMismatch Nothing = EffectMismatch [] []
+
+concreteEffectLabels typ = head ++ tailList
+  where
+    (head, tail) = extractOrderedEffect typ
+    tailList =
+      if isEffectEmpty tail || isMeta tail then [] else [tail]
+
+    isMeta (TVar (TypeVar _ kind Meta)) = True
+    isMeta _ = False
+
+effectMismatchUnexpected unexpected = EffectMismatch (concreteEffectLabels unexpected) []
+
+effectMismatchMissing missing = EffectMismatch [] (concreteEffectLabels missing)
+
+noMatchTypes = NoMatch Nothing
+
 data UnifyError
-  = NoMatch
+  = NoMatch (Maybe EffectMismatch)
   | NoMatchKind
   | NoMatchSkolem Kind
-  | NoMatchEffect Type Type
+  | NoMatchEffect Type Type EffectMismatch
   | NoSubsume
   | Infinite
   | NoArgMatch Int Int
diff --git a/test/algeff/wrong/eff-rec2.kk.out b/test/algeff/wrong/eff-rec2.kk.out
index 10d228b12..f34208317 100644
--- a/test/algeff/wrong/eff-rec2.kk.out
+++ b/test/algeff/wrong/eff-rec2.kk.out
@@ -6,4 +6,5 @@ test/algeff/wrong/eff-rec2@kk(39,32): type error: effects do not match
  @@@
  }
  inferred effect: <console,div,exn|_e>
- expected effect: <exn,console>
\ No newline at end of file
+ expected effect: <exn,console>
+ unexpected : div
diff --git a/test/type/wrong/effect3.kk b/test/type/wrong/effect3.kk
new file mode 100644
index 000000000..4bee5a1df
--- /dev/null
+++ b/test/type/wrong/effect3.kk
@@ -0,0 +1,3 @@
+fun main(): io-noexn ()
+  println("")
+  throw("error!")
diff --git a/test/type/wrong/effect3.kk.out b/test/type/wrong/effect3.kk.out
new file mode 100644
index 000000000..1769cba48
--- /dev/null
+++ b/test/type/wrong/effect3.kk.out
@@ -0,0 +1,10 @@
+test/type/wrong/effect3.kk(1,23): type error: effects do not match
+  context        : fun main(): io-noexn ()
+                   println("")
+                   throw("error!")
+  term           : 
+                   println("")
+                   throw("error!")
+  inferred effect: <exn,console/console|_e>
+  expected effect: io-noexn
+  unexpected     : exn
diff --git a/test/type/wrong/effect4.kk b/test/type/wrong/effect4.kk
new file mode 100644
index 000000000..e647e21c4
--- /dev/null
+++ b/test/type/wrong/effect4.kk
@@ -0,0 +1,8 @@
+fun io-action(): io ()
+  ()
+
+fun main(action: () -> <io-noexn|e> ()): <io|e> int
+  var x := 1
+  io-action()
+  action()
+  x
diff --git a/test/type/wrong/effect4.kk.out b/test/type/wrong/effect4.kk.out
new file mode 100644
index 000000000..9d28defe6
--- /dev/null
+++ b/test/type/wrong/effect4.kk.out
@@ -0,0 +1,7 @@
+test/type/wrong/effect4.kk(6, 3): type error: effects do not match
+  context        : io-action()
+  term           : io-action()
+  inferred effect: <local<_h>,alloc<global>,console,div,fsys,ndet,net,read<global>,ui,write<global>|$e>
+  expected effect: <alloc<global>,console,div,exn,fsys,ndet,net,read<global>,ui,write<global>,local<_h>|_e1>
+  missing : exn
+            Consider using mask or adding it to the function's effect type
diff --git a/test/type/wrong/scheduler1.kk.out b/test/type/wrong/scheduler1.kk.out
index d778f36ba..a0c431b29 100644
--- a/test/type/wrong/scheduler1.kk.out
+++ b/test/type/wrong/scheduler1.kk.out
@@ -3,4 +3,5 @@ test/type/wrong/scheduler1@kk(18, 7): type error: effects do not match
  term : q
  inferred effect: <alloc<global>|_e>
  expected effect: total
- because : Polymorphic values cannot have an effect
\ No newline at end of file
+ unexpected : alloc<global>
+ because : Polymorphic values cannot have an effect
diff --git a/test/type/wrong/scheduler5.kk.out b/test/type/wrong/scheduler5.kk.out
index 15814584d..fd2e78286 100644
--- a/test/type/wrong/scheduler5.kk.out
+++ b/test/type/wrong/scheduler5.kk.out
@@ -2,4 +2,6 @@ test/type/wrong/scheduler5@kk(40, 9): type error: effects do not match
  context : spawn(f)
  term : f
  inferred effect: <pure,process,st<global>|$e>
- expected effect: <pure,alloc<global>,process,read<global>,write<global>,exn>
\ No newline at end of file
+ expected effect: <pure,alloc<global>,process,read<global>,write<global>,exn>
+ missing : exn
+          Consider using mask or adding it to the function's effect type
diff --git a/test/type/wrong/st1.kk.out b/test/type/wrong/st1.kk.out
index b8b44f319..665c00497 100644
--- a/test/type/wrong/st1.kk.out
+++ b/test/type/wrong/st1.kk.out
@@ -3,4 +3,5 @@ test/type/wrong/st1@kk(1, 9): type error: effects do not match
  term : ref
  inferred effect: <alloc<_h>|_e>
  expected effect: total
- because : Generalized values cannot have an effect
\ No newline at end of file
+ unexpected : alloc<_h>
+ because : Generalized values cannot have an effect
diff --git a/test/type/wrong/val1.kk.out b/test/type/wrong/val1.kk.out
index ecef28304..f2ec0fa9b 100644
--- a/test/type/wrong/val1.kk.out
+++ b/test/type/wrong/val1.kk.out
@@ -3,4 +3,5 @@ test/type/wrong/val1@kk(2, 7): type error: effects do not match
  term : r
  inferred effect: <alloc<global>|_e>
  expected effect: total
- because : Polymorphic values cannot have an effect
\ No newline at end of file
+ unexpected : alloc<global>
+ because : Polymorphic values cannot have an effect