Skip to content

add effect type mismatch hints #791

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
timbertson wants to merge 1 commit into
base: dev
Choose a base branch
from
Open

add effect type mismatch hints #791

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 31 additions & 4 deletions src/Type/InferMonad.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -599,6 +599,7 @@ unifyError' env context range err tp1 tp2
,(text ("inferred " ++ nameType), nice2)
]
++ nomatch
++ effectDiffs
++ extra
++ hint
)
Expand Down Expand Up @@ -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))
Expand All @@ -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"
Expand Down
68 changes: 52 additions & 16 deletions src/Type/Unify.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ module Type.Unify ( Unify, UnifyError(..), runUnify, runUnifyEx
, matchArguments
, matchShape, pureMatchShape
, extractNormalizeEffect
, unexpectedEffectLabels
, missingEffectLabels
) where

import Control.Applicative
Expand Down Expand Up @@ -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 ()

Expand All @@ -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)
Expand All @@ -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,
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion test/algeff/wrong/eff-rec2.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 3 additions & 0 deletions test/type/wrong/effect3.kk
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
fun main(): io-noexn ()
println("")
throw("error!")
10 changes: 10 additions & 0 deletions test/type/wrong/effect3.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
8 changes: 8 additions & 0 deletions test/type/wrong/effect4.kk
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
fun io-action(): io ()
()

fun main(action: () -> <io-noexn|e> ()): <io|e> int
var x := 1
io-action()
action()
x
7 changes: 7 additions & 0 deletions test/type/wrong/effect4.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
3 changes: 2 additions & 1 deletion test/type/wrong/scheduler1.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 3 additions & 1 deletion test/type/wrong/scheduler5.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 2 additions & 1 deletion test/type/wrong/st1.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 2 additions & 1 deletion test/type/wrong/val1.kk.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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