add effect type mismatch hints:

timbertson · timbertson · commit 7af9d0a331c3 · 2025-09-07T21:33:43.000+10:00
- unexpected effects
 - missing effects when a skolem fails to unify
diff --git a/src/Type/InferMonad.hs b/src/Type/InferMonad.hs
@@ -571,8 +571,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
@@ -589,6 +589,7 @@ unifyError' env context range err tp1 tp2
                ,(text ("inferred " ++ nameType), nice2)
                ]
                ++ nomatch
+               ++ effectDiffs
                ++ extra
                ++ hint
               )
@@ -617,10 +618,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))
@@ -630,7 +657,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
@@ -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,15 +126,15 @@ 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
                       let (fpars,rest) = splitAt (length fixed) parsNotNamedArg
                       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
@@ -272,8 +274,9 @@ unify f1@(TFun args1 eff1 res1) f2@(TFun args2 eff2 res2) | length args1 == leng
        withError (effErr) (unify eff1 eff2)
   where
     -- specialize to sub-part of the type for effect unification errors
-    effErr NoMatch              = NoMatchEffect eff1 eff2
-    effErr (NoMatchEffect _ _)  = NoMatchEffect eff1 eff2
+    effErr (NoMatch diff) = NoMatchEffect eff1 eff2 (maybeEffectMismatch diff)
+
+    effErr (NoMatchEffect _ _ diff)  = NoMatchEffect eff1 eff2 diff
     effErr err                  = err
 
 -- quantified types
@@ -321,9 +324,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
@@ -337,7 +350,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)
@@ -477,11 +490,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
@@ -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>
+ expected effect: <exn,console>
+ unexpected : div
diff --git a/test/type/wrong/effect3.kk 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
@@ -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
@@ -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
@@ -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
@@ -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
+ 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
@@ -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>
+ 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
@@ -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
+ 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
@@ -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
+ unexpected : alloc<global>
+ because : Polymorphic values cannot have an effect

Original file line number	Diff line number	Diff line change
`@@ -6,4 +6,5 @@ test/algeff/wrong/eff-rec2@kk(39,32): type error: effects do not match`
`6`	`6`	`@@@`
`7`	`7`	`}`
`8`	`8`	`inferred effect: <console,div,exn\|_e>`
`9`		`- expected effect: <exn,console>`
	`9`	`+ expected effect: <exn,console>`
	`10`	`+ unexpected : div`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+fun main(): io-noexn ()`
	`2`	`+ println("")`
	`3`	`+ throw("error!")`