Skip to content

Commit

Permalink
Merge pull request #1596 from actonlang/improve-typeerrormsgs-4
Browse files Browse the repository at this point in the history
Improve typeerrormsgs 4
  • Loading branch information
sydow authored Dec 5, 2023
2 parents 9224b58 + 1eac0a4 commit 05c3993
Show file tree
Hide file tree
Showing 27 changed files with 347 additions and 190 deletions.
78 changes: 78 additions & 0 deletions compiler/Acton/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -484,6 +484,17 @@ findQName (GName m n) env
Nothing -> noItem m n -- error ("## Failed lookup of " ++ prstr n ++ " in module " ++ prstr m)
Nothing -> noModule m -- error ("## Failed lookup of module " ++ prstr m)

findSigLoc n env = findSL (names env)
where findSL ((n',t):ps)
| NSig{} <- t, n==n' = Just (loc n')
| otherwise = findSL ps
findSL [] = Nothing

findDefLoc n env = findSL (names env)
where findSL ((n',t):ps)
| NDef{} <- t, n==n' = Just (loc n')
| otherwise = findSL ps
findSL [] = Nothing

findName n env = findQName (NoQ n) env

Expand Down Expand Up @@ -1211,3 +1222,70 @@ err3 l xs s = err l (s ++ " " ++ prstrs xs)

notYetExpr e = notYet (loc e) e

stripQual q = [ Quant v [] | Quant v us <- q ]


class Simp a where
simp :: EnvF x -> a -> a

instance (Simp a) => Simp [a] where
simp env = map (simp env)

instance Simp TSchema where
simp env (TSchema l q t) = TSchema l q' (substIteratively s $ simp env' t)
where (q', s) = simpQuant env (simp env' q) (tyfree t)
env' = defineTVars (stripQual q) env

simpQuant env q vs0 = (subst s [ Quant v ps | Quant v ps <- q2, not $ null ps ], s)
where (q1,q2) = partition isEX q
isEX (Quant v [p]) = length (filter (==v) vs) == 1
isEX _ = False
vs = concat [ tyfree ps | Quant v ps <- q ] ++ vs0
s = s1 ++ s2
s1 = [ (v, tCon p) | Quant v [p] <- q1 ] -- Inline existentials
s2 = univars `zip` beautyvars -- Beautify univars
univars = filter univar $ qbound q2
beautyvars = map tVar $ tvarSupply \\ tvarScope env

instance Simp QBind where
simp env (Quant v ps) = Quant v (simp env ps)

instance Simp WTCon where
simp env (w, c) = (w, simp env c)

instance Simp (Name, NameInfo) where
simp env (n, NSig sc dec) = (n, NSig (simp env sc) dec)
simp env (n, NDef sc dec) = (n, NDef (simp env sc) dec)
simp env (n, NVar t) = (n, NVar (simp env t))
simp env (n, NSVar t) = (n, NSVar (simp env t))
simp env (n, NClass q us te) = (n, NClass (simp env' q) (simp env' us) (simp env' te))
where env' = defineTVars (stripQual q) env
simp env (n, NProto q us te) = (n, NProto (simp env' q) (simp env' us) (simp env' te))
where env' = defineTVars (stripQual q) env
simp env (n, NExt q c us te) = (n, NExt q' (subst s $ simp env' c) (subst s $ simp env' us) (subst s $ simp env' te))
where (q', s) = simpQuant env (simp env' q) (tyfree c ++ tyfree us ++ tyfree te)
env' = defineTVars (stripQual q) env
simp env (n, NAct q p k te) = (n, NAct (simp env' q) (simp env' p) (simp env' k) (simp env' te))
where env' = defineTVars (stripQual q) env
simp env (n, i) = (n, i)

instance Simp Type where
simp env (TCon l c) = TCon l (simp env c)
simp env (TFun l fx p k t) = TFun l (simp env fx) (simp env p) (simp env k) (simp env t)
simp env (TTuple l p k) = TTuple l (simp env p) (simp env k)
simp env (TOpt l t) = TOpt l (simp env t)
simp env (TRow l k n t r) = TRow l k n (simp env t) (simp env r)
simp env t = t

instance Simp TCon where
simp env (TC n ts) = TC (simp env n) (simp env ts)

instance Simp QName where
simp env (GName m n)
| inBuiltin env = NoQ n
| Just m == thismod env = NoQ n
simp env n
| not $ null aliases = NoQ $ head aliases
| otherwise = n
where aliases = [ n1 | (n1, NAlias n2) <- names env, n2 == n ]

44 changes: 28 additions & 16 deletions compiler/Acton/Solver.hs
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ solve' env select hist te tt eq cs
--traceM ("### var goals: " ++ show (sum [ length alts | RVar t alts <- vargoals ]))
sequence [ unify (DfltInfo (loc t) 2 Nothing []) t t' | RVar t alts <- vargoals, t' <- alts ]
proceed hist cs
| any not keep_evidence = noSolve Nothing [] keep_cs
| any not keep_evidence = noSolve0 Nothing [] keep_cs
| null solve_cs || null goals = return (keep_cs, eq)
| otherwise = do st <- currentState
--traceM ("## keep:\n" ++ render (nest 8 $ vcat $ map pretty keep_cs))
Expand Down Expand Up @@ -167,9 +167,8 @@ solve' env select hist te tt eq cs
cs' = if length cs == 1 then cs else filter (not . useless vs) cs
vs' = filter (\ v -> length (filter (\c -> v `elem` tyfree c) cs') > 1) (nub(tyfree cs')) -- is this necessary??
cs' <- msubstWith (zip vs' ts) cs'
cs' <- wildify cs'
noSolve (Just t) (take (length vs') ts) cs'
tryAlts st _ [] = noSolve Nothing [] cs
noSolve0 (Just t) (take (length vs') ts) cs'
tryAlts st _ [] = noSolve0 Nothing [] cs
tryAlts st t0 (t:ts) = tryAlt t0 t `catchError` const ({-traceM ("=== ROLLBACK " ++ prstr t0) >> -}rollbackState st >> tryAlts st t0 ts)
tryAlt t0 (TCon _ c)
| isProto env (tcname c) = do p <- instwildcon env c
Expand Down Expand Up @@ -490,7 +489,7 @@ reduce' env eq (Seal _ t@(TFX _ fx))
reduce' env eq (Seal info t) = reduce env eq (map (Seal info) ts)
where ts = leaves t

reduce' env eq c = noRed c
reduce' env eq c = noRed0 c


solveImpl env wit w t p = do (cs,p',we) <- instWitness env t wit
Expand Down Expand Up @@ -643,10 +642,10 @@ cast' env info t1@(TFX _ fx1) t2@(TFX _ fx2)

cast' env _ (TNil _ k1) (TNil _ k2)
| k1 == k2 = return ()
cast' env info (TNil _ _) r2@(TRow _ k n t2 r2')
= posElemNotFound True info n
cast' env info t1@(TNil _ _) r2@(TRow _ k n t2 r2')
= posElemNotFound0 env True (Cast info t1 t2) n
cast' env info r1@(TRow _ k n _ _) r2@(TNil _ _)
= posElemNotFound False info n
= posElemNotFound0 env False (Cast info r1 r2) n
cast' env info (TVar _ tv) r2@(TNil _ k) = do substitute tv (tNil k)
cast env info (tNil k) r2
cast' env info r1 (TRow _ k n t2 r2) = do (t1,r1') <- findElem info k (tNil k) n r1 r2
Expand Down Expand Up @@ -682,15 +681,28 @@ cast' env info t1 t2@(TVar _ tv)
cast' env info t1@(TVar _ tv) t2 = cast' env info (tCon tc) t2
where tc = findTVBound env tv

cast' env info t1 t2@(TVar _ tv) = noRed (Cast info t1 t2)
cast' env info t1 t2@(TVar _ tv) = noRed0 (Cast info t1 t2)

cast' env info t1 (TOpt _ t2) = cast env info t1 t2 -- Only matches when t1 is NOT a variable

cast' env info t1 t2 = do t1' <- wildify t1
t2' <- wildify t2
info' <- wildify info
noRed (Cast info' t1' t2')
cast' env info t1 t2 = noRed0 (Cast info t1 t2)

noRed0 c = do c <- msubst c
c <- wildify c
noRed c

noSolve0 mbt vs cs = do mbt <- msubst mbt
cs <- msubst cs
mbt <- wildify mbt
cs <- wildify cs
noSolve mbt vs cs

posElemNotFound0 env b c n = do c <- msubst c
c <- wildify c
posElemNotFound b (s c) n
where s c = case info c of
DeclInfo l1 l2 n sc msg -> c {info = DeclInfo l1 l2 n (simp env sc) msg}
_ -> c
{-
splitInfo info t1 t2 = case info of
DfltInfo _ _ (Just (List _ (Elem e : es))) ts ->
Expand Down Expand Up @@ -747,10 +759,10 @@ sub' env info eq w r1@(TNil _ k1) r2@(TNil _ k2)
| k1 == k2 = return (idwit env w tUnit tUnit : eq)

-- existing expected Match labels in the order of the expected row
sub' env info eq w (TNil _ _) r2@(TRow _ k n t2 r2')
= posElemNotFound True info n
sub' env info eq w r1@(TNil _ _) r2@(TRow _ k n t2 r2')
= posElemNotFound0 env True (Sub info w r1 r2) n -- posElemNotFound True info n
sub' env info eq w r1@(TRow _ k n _ _) r2@(TNil _ _)
= posElemNotFound False info n
= posElemNotFound0 env False (Sub info w r1 r2) n
sub' env info eq w r1 r2@(TRow _ k n t2 r2')
= do (t1,r1') <- findElem info k (tNil k) n r1 r2'
wt <- newWitness
Expand Down
22 changes: 11 additions & 11 deletions compiler/Acton/Subst.hs
Original file line number Diff line number Diff line change
Expand Up @@ -93,7 +93,7 @@ instance Subst a => Subst (Name,a) where
tyfree (n, t) = tyfree t
tybound (n, t) = tybound t

instance (Subst a, Subst b) => Subst (Name,a,b) where
instance (Subst a, Subst b) => Subst (QName,a,b) where
msubst (n, t, u) = (,,) <$> return n <*> msubst t <*> msubst u
tyfree (n, t, u) = tyfree t ++ tyfree u
tybound (n, t, u) = tybound t ++ tybound u
Expand All @@ -116,21 +116,21 @@ instance Subst Constraint where
msubst (Mut info t1 n t2) = Mut <$> msubst info <*> msubst t1 <*> return n <*> msubst t2
msubst (Seal info t) = Seal <$> msubst info <*> msubst t

tyfree (Cast _ t1 t2) = tyfree t1 ++ tyfree t2
tyfree (Sub _ w t1 t2) = tyfree t1 ++ tyfree t2
tyfree (Impl _ w t p) = tyfree t ++ tyfree p
tyfree (Sel _ w t1 n t2) = tyfree t1 ++ tyfree t2
tyfree (Mut _ t1 n t2) = tyfree t1 ++ tyfree t2
tyfree (Seal _ t) = tyfree t
tyfree (Cast info t1 t2) = tyfree info ++ tyfree t1 ++ tyfree t2
tyfree (Sub info w t1 t2) = tyfree info ++ tyfree t1 ++ tyfree t2
tyfree (Impl info w t p) = tyfree info ++ tyfree t ++ tyfree p
tyfree (Sel info w t1 n t2) = tyfree info ++ tyfree t1 ++ tyfree t2
tyfree (Mut info t1 n t2) = tyfree info ++ tyfree t1 ++ tyfree t2
tyfree (Seal info t) = tyfree info ++ tyfree t


instance Subst ErrInfo where
msubst (DfltInfo l n mbe ts) = DfltInfo l n <$> msubst mbe <*> msubst ts
msubst (DeclInfo l1 l2 d t msg) = DeclInfo l1 l2 <$> msubst d <*> msubst t <*> return msg
msubst (DeclInfo l1 l2 n t msg) = DeclInfo l1 l2 n <$> msubst t <*> return msg
msubst info = return info

tyfree (DfltInfo l n mbe ts) = tyfree mbe ++ tyfree ts
tyfree (DeclInfo l1 l2 d t msg) = tyfree d ++ tyfree t
tyfree (DeclInfo l1 l2 n t msg) = tyfree t
tyfree _ = []

instance Subst TSchema where
Expand Down Expand Up @@ -195,8 +195,8 @@ msubstWith s x = do s0 <- getSubstitution
setSubstitution s0
return x'

wildify :: Subst a => a -> TypeM a
wildify a = msubstWith (zip (tyfree a) (repeat tWild)) a
wildify :: (Subst a) => a -> TypeM a
wildify a = msubstWith (zip (tyfree a \\ tybound a) (repeat tWild)) a

testMsubstRenaming = do
putStrLn ("p1: " ++ render (pretty (runTypeM p1)))
Expand Down
10 changes: 5 additions & 5 deletions compiler/Acton/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -253,9 +253,9 @@ data Constraint = Cast {info :: ErrInfo, type1 :: Type, type2 :: Type}

type Constraints = [Constraint]

data ErrInfo = DfltInfo {errloc :: SrcLoc, ident :: Int, iexpr :: Maybe Expr, typings :: [(Name,TSchema,Type)]}
| DeclInfo {errloc :: SrcLoc, otherloc :: SrcLoc, idecl :: Decl, itype :: Type, imsg :: String}
| Simple {errloc ::SrcLoc, imsg :: String}
data ErrInfo = DfltInfo {errloc :: SrcLoc, errno :: Int, errexpr :: Maybe Expr, errinsts :: [(QName,TSchema,Type)]}
| DeclInfo {errloc :: SrcLoc, errloc2 :: SrcLoc, errname :: Name, errschema :: TSchema, errmsg :: String}
| Simple {errloc ::SrcLoc, errmsg :: String}
deriving (Eq,Show,Read,Generic,NFData)

type WPath = [Either QName QName]
Expand Down Expand Up @@ -589,12 +589,12 @@ instance HasLoc ErrInfo where
loc (DeclInfo l _ _ _ _) = l

instance HasLoc PosArg where
loc (PosArg e p) = loc e
loc (PosArg e p) = loc e `upto` loc p
loc (PosStar e) = loc e
loc PosNil = NoLoc

instance HasLoc KwdArg where
loc (KwdArg n e p) = loc n `upto` loc e
loc (KwdArg n e k) = loc n `upto` loc k
loc (KwdStar e) = loc e
loc KwdNil = NoLoc

Expand Down
24 changes: 13 additions & 11 deletions compiler/Acton/TypeM.hs
Original file line number Diff line number Diff line change
Expand Up @@ -162,24 +162,24 @@ explainViolation c = case info c of
Impl _ _ t p -> intro False t mbe <+> text "does not implement" <+> pretty p
Sel _ _ t n t0 -> intro False t mbe <+> text "does not have an attribute" <+> pretty n <+> text "with type" <+> pretty t0
_ -> pretty c <+> text "does not hold")
DeclInfo _ _ _ t msg -> text msg $+$ text "Function inferred to have type"<+> pretty t
DeclInfo _ _ n sc msg -> text msg $+$ pretty n <+> text "is inferred to have a type of the form"<+> pretty sc

explainRequirement b c = case info c of
Simple l s -> text s
DfltInfo l n mbe ts ->
(if ts /= []
then text (concatMap (\(n,s,t) -> Pretty.print n ++ " has had its polymorphic type "
++ Pretty.print s ++ " instantiated to " ++ Pretty.print t) ts++", so") -- s is printed with internal typevars, not A, B...
++ Pretty.print s ++ " instantiated to " ++ Pretty.print t) ts++", so ")

else empty) $+$
else empty) Pretty.<>
(case c of
Cast _ t1 t2 -> intro b t1 mbe <+> text "must be a subclass of" <+> pretty t2
Sub i _ t1 t2 -> intro b t1 mbe <+> text "must be a subtype of" <+> pretty t2
Impl _ _ t p -> intro b t mbe <+> text "must implement" <+> pretty p
Sel _ _ t n t0 -> intro b t mbe <+> text "must have an attribute" <+> pretty n <+> text "with type" <+> pretty t0
Pretty.<> text "; no such type is known."
_ -> pretty c <+> text "must hold")
DeclInfo _ _ _ t msg -> text msg $+$ text "Function inferred to have type"<+> pretty t
DeclInfo _ _ n sc msg -> text msg $+$ pretty n <+> text "is inferred to have a type of the form"<+> pretty sc



Expand Down Expand Up @@ -208,17 +208,15 @@ typeError (NoMut n) = [(loc n, render (text "Non @property attr
typeError (LackSig n) = [(loc n, render (text "Declaration lacks accompanying signature"))]
typeError (LackDef n) = [(loc n, render (text "Signature lacks accompanying definition"))]
typeError (NoRed c)
| DeclInfo l1 l2 _ t _ <- info c = [(l1,""), (l2,render (explainViolation c))]
| DeclInfo l1 l2 _ _ _ <- info c = [(l1,""), (l2,render (explainViolation c))]
| otherwise = [(loc c, render (explainViolation c))]
typeError (NoSolve mbt vs cs) = case length cs of
0 -> [(NoLoc, "Unable to give good error message: please report example")]
1 -> (NoLoc, "Cannot satisfy the following constraint:\n") : map (mkReq False) cs
_ -> (NoLoc, "Cannot satisfy the following simultaneous constraints for the unknown "
++ (if length vs==1 then "type " else "types ") ++ render(commaList vs) ++":\n")
: map (mkReq True) (cs2++cs1)
where mkReq b c = (newLoc c, render (explainRequirement b c))
(cs1,cs2) = partition (\c -> null $ typings(info c)) cs
newLoc c = if null (typings (info c)) then loc c else loc(fst3(head(typings (info c))))
: map (mkReq True) cs
where mkReq b c = (loc c, render (explainRequirement b c))
fst3 (a,_,_) = a

typeError (NoUnify info t1 t2) = case (loc t1, loc t2) of
Expand All @@ -241,5 +239,9 @@ noRed c = throwError $ NoRed c
noSolve mbt vs cs = throwError $ NoSolve mbt vs cs
noUnify info t1 t2 = throwError $ NoUnify info t1 t2

posElemNotFound True info n = throwError $ PosElemNotFound info "Too few positional elements"
posElemNotFound False info n = throwError $ PosElemNotFound info "Too many positional elements"
posElemNotFound True c n = case info c of
DeclInfo{} -> throwError $ NoRed (c{info = (info c){errmsg = errmsg(info c)++" (too few arguments in call)"}})
info -> throwError $ PosElemNotFound info "Too few positional elements"
posElemNotFound False c n = case info c of
DeclInfo{} -> throwError $ NoRed (c{info = (info c){errmsg = errmsg(info c)++" (too many arguments in call)"}})
info -> throwError $ PosElemNotFound info "Too many positional elements"
Loading

0 comments on commit 05c3993

Please sign in to comment.