Output all type errors instead of just the first one where possible

by using `Result` instead of `M` where possible, because
Applicative instance for `Result` accumulates errors.
This commit is contained in:
Tomas Mikula 2019-11-14 23:49:20 +01:00
parent de5f87bbd2
commit 24b3af8136
4 changed files with 64 additions and 12 deletions

View File

@ -38,6 +38,8 @@ module Unison.Typechecker.Context
, Suggestion(..)
, SuggestionMatch(..)
, isExact
, typeErrors
, infoNotes
)
where
@ -138,6 +140,12 @@ instance Monad (Result v loc) where
btw' :: InfoNote v loc -> Result v loc ()
btw' note = Success (Seq.singleton note) ()
typeError :: Cause v loc -> Result v loc a
typeError cause = TypeError (pure $ ErrorNote cause mempty) mempty
compilerBug :: CompilerBug v loc -> Result v loc a
compilerBug bug = CompilerBug bug mempty mempty
typeErrors :: Result v loc a -> Seq (ErrorNote v loc)
typeErrors = \case
TypeError es _ -> nonEmptySeqToSeq es
@ -616,11 +624,10 @@ shouldPerformAbilityCheck t = do
pure $ all (/= t) skip
compilerCrash :: CompilerBug v loc -> M v loc a
compilerCrash bug = liftResult $ CompilerBug bug mempty mempty
compilerCrash bug = liftResult $ compilerBug bug
failWith :: Cause v loc -> M v loc a
failWith cause =
liftResult $ TypeError (pure $ ErrorNote cause mempty) mempty
failWith cause = liftResult $ typeError cause
compilerCrashResult :: CompilerBug v loc -> Result v loc a
compilerCrashResult bug = CompilerBug bug mempty mempty
@ -1608,7 +1615,7 @@ abilityCheck requested = do
abilityCheck' (apply ctx <$> ambient >>= Type.flattenEffects)
(apply ctx <$> requested' >>= Type.flattenEffects)
verifyDataDeclarations :: (Var v, Ord loc) => DataDeclarations v loc -> M v loc ()
verifyDataDeclarations :: (Var v, Ord loc) => DataDeclarations v loc -> Result v loc ()
verifyDataDeclarations decls = forM_ (Map.toList decls) $ \(_ref, decl) -> do
let ctors = DD.constructors decl
forM_ ctors $ \(_ctorName,typ) -> verifyClosed typ id
@ -1628,25 +1635,25 @@ synthesizeClosed abilities lookupType term0 = let
Left missingRef ->
compilerCrashResult (UnknownTermReference missingRef)
Right term -> run [] datas effects $ do
verifyDataDeclarations datas
verifyDataDeclarations (DD.toDataDecl <$> effects)
verifyClosedTerm term
liftResult $ verifyDataDeclarations datas
*> verifyDataDeclarations (DD.toDataDecl <$> effects)
*> verifyClosedTerm term
synthesizeClosed' abilities term
verifyClosedTerm :: forall v loc . Ord v => Term v loc -> M v loc ()
verifyClosedTerm :: forall v loc . Ord v => Term v loc -> Result v loc ()
verifyClosedTerm t = do
ok1 <- verifyClosed t id
let freeTypeVars = Map.toList $ Term.freeTypeVarAnnotations t
reportError (v, locs) = for_ locs $ \loc ->
failWith (UnknownSymbol loc (TypeVar.underlying v))
typeError (UnknownSymbol loc (TypeVar.underlying v))
for_ freeTypeVars reportError
when (not ok1 || (not . null) freeTypeVars) $ compilerCrash (OtherBug "impossible")
when (not ok1 || (not . null) freeTypeVars) $ compilerBug (OtherBug "impossible")
verifyClosed :: (Traversable f, Ord v) => ABT.Term f v a -> (v -> v2) -> M v2 a Bool
verifyClosed :: (Traversable f, Ord v) => ABT.Term f v a -> (v -> v2) -> Result v2 a Bool
verifyClosed t toV2 =
let isBoundIn v t = Set.member v (snd (ABT.annotation t))
loc t = fst (ABT.annotation t)
go t@(ABT.Var' v) | not (isBoundIn v t) = failWith (UnknownSymbol (loc t) $ toV2 v)
go t@(ABT.Var' v) | not (isBoundIn v t) = typeError (UnknownSymbol (loc t) $ toV2 v)
go _ = pure True
in all id <$> ABT.foreachSubterm go (ABT.annotateBound t)

View File

@ -20,6 +20,7 @@ import qualified Unison.Test.TermPrinter as TermPrinter
import qualified Unison.Test.Type as Type
import qualified Unison.Test.TypePrinter as TypePrinter
import qualified Unison.Test.Typechecker as Typechecker
import qualified Unison.Test.Typechecker.Context as Context
import qualified Unison.Test.Typechecker.TypeError as TypeError
import qualified Unison.Test.UnisonSources as UnisonSources
import qualified Unison.Test.Util.Bytes as Bytes
@ -50,6 +51,7 @@ test = tests
, Var.test
, Codebase.test
, Typechecker.test
, Context.test
]
main :: IO ()

View File

@ -0,0 +1,42 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
module Unison.Test.Typechecker.Context ( test )
where
import Data.Foldable ( for_ )
import EasyTest
import Unison.Symbol ( Symbol )
import qualified Unison.Typechecker.Context as Context
import qualified Unison.Term as Term
import qualified Unison.Type as Type
import qualified Unison.Var as Var
test :: Test ()
test = scope "context" $ tests
[ scope "verifyClosedTerm" verifyClosedTermTest
]
type TV = Context.TypeVar Symbol ()
verifyClosedTermTest :: Test ()
verifyClosedTermTest = tests
[ scope "report-all-free-vars" $
let
a = Var.named @Symbol "a"
b = Var.named @Symbol "b"
a' = Var.named @TV "a'"
b' = Var.named @TV "b'"
-- (a : a')(b : b')
t = Term.app()
(Term.ann() (Term.var() a) (Type.var() a'))
(Term.ann() (Term.var() b) (Type.var() b'))
res = Context.synthesizeClosed [] mempty t
errors = Context.typeErrors res
expectUnknownSymbol (Context.ErrorNote cause _) = case cause of
Context.UnknownSymbol _ _ -> ok
e -> crash $ "Unexpected type error " <> show e
in do
expectEqual 4 (length errors) -- there are 4 unknown symbols: a, a', b, b'
for_ errors expectUnknownSymbol
]

View File

@ -299,6 +299,7 @@ executable tests
Unison.Test.TypePrinter
Unison.Test.Typechecker
Unison.Test.Typechecker.Components
Unison.Test.Typechecker.Context
Unison.Test.Typechecker.TypeError
Unison.Test.UnisonSources
Unison.Test.Util.Bytes