unisonweb/unison
1
0
Fork 0
mirror of https://github.com/unisonweb/unison.git synced 2024-09-17 13:27:30 +03:00
Code Issues Projects Releases Wiki Activity

sketched out cases for ExistentialMismatch (if/vector/case)*

Browse Source 
* the checks yield false positives, see https://app.asana.com/0/781300632285932/783413200023835/f

- factored out "fromOverHere" to do a right thing for 0, 1, 2 other locations
- still haven't found a great model for extractors, but fixing the above bug may lead to something.
This commit is contained in:
Arya Irani 2018-08-17 14:30:36 -04:00
parent b1bba8f8cc
commit 1c682f55b5
5 changed files with 195 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

174
parser-typechecker/src/Unison/PrintError.hs
View File

@ -39,10 +39,11 @@ import qualified Unison.Util.AnnotatedText as AT
import Unison.Util.ColorText (StyledText)
import qualified Unison.Util.ColorText as Color
import Unison.Util.Monoid (intercalateMap)
import Unison.Util.Monoid (whenM)
-- import Unison.Util.Monoid (whenM)
import Unison.Util.Range (Range (..))
import Unison.Var (Var)
import qualified Unison.Var as Var
-- import Debug.Trace
data Env = Env { referenceNames :: Map R.Reference String
, constructorNames :: Map (R.Reference, Int) String }
@ -50,20 +51,29 @@ data Env = Env { referenceNames :: Map R.Reference String
env0 :: Env
env0 = Env mempty mempty
data BooleanMismatch = CondMismatch | AndMismatch | OrMismatch
data BooleanMismatch = CondMismatch | AndMismatch | OrMismatch -- | GuardMismatch
data ExistentialMismatch = IfBody | VectorBody | CaseBody
data TypeError v loc
= Mismatch { overallType1 :: C.Type v loc
, overallType2 :: C.Type v loc
, leaf1 :: C.Type v loc
, leaf2 :: C.Type v loc
= Mismatch { foundType :: C.Type v loc -- overallType1
, expectedType :: C.Type v loc -- overallType2
, foundLeaf :: C.Type v loc -- leaf1
, expectedLeaf :: C.Type v loc -- leaf2
, mismatchSite :: loc
, note :: C.Note v loc
}
| BooleanMismatch { booleanMismatch :: BooleanMismatch
, mismatchSite :: loc
, mismatchedType :: C.Type v loc
, note :: C.Note v loc }
, mismatchSite :: loc
, foundType :: C.Type v loc
, note :: C.Note v loc
}
| ExistentialMismatch { existentialMismatch :: ExistentialMismatch
, expectedType :: C.Type v loc
, expectedLoc :: loc
, foundType :: C.Type v loc
, mismatchSite :: loc
, note :: C.Note v loc
}
| AbilityCheckFailure { ambient :: [C.Type v loc]
, requested :: [C.Type v loc]
, abilityCheckFailureSite :: loc
@ -89,17 +99,62 @@ mustBeBool initial env src mismatchSite mismatchedType =
[ " ", AT.Text $ Color.type1 "Boolean", ", but this one is "
, AT.Text . Color.type2 . renderType' env $ mismatchedType
, ":\n\n"
-- , showSourceMaybes src
-- [(,Color.Type2) <$> rangeForAnnotated mismatchSite
-- ,(,Color.Type2) <$> rangeForAnnotated mismatchedType]
-- , "\n\n"
, annotatedAsStyle Color.Type2 src mismatchSite
, showSourceMaybes src [siteS]
, "\n"
] ++ whenM (mismatchSite /= ABT.annotation mismatchedType) [
"from over here:\n\n"
, annotatedAsStyle Color.Type2 src (ann mismatchedType)
, "\n\n"
]
] ++ fromOverHere' src [typeS] [siteS]
where siteS = styleAnnotated Color.Type2 mismatchSite
typeS = styleAnnotated Color.Type2 mismatchedType
fromOverHere' :: Ord a
=> String
-> [Maybe (Range, a)]
-> [Maybe (Range, a)]
-> [AT.Section a]
fromOverHere' s spots0 removing =
fromOverHere s (catMaybes spots0) (catMaybes removing)
fromOverHere :: Ord a
=> String
-> [(Range, a)]
-> [(Range, a)]
-> [AT.Section a]
fromOverHere src spots0 removing =
let spots = toList $ Set.fromList spots0 Set.\\ Set.fromList removing
in case length spots of
0 -> mempty
1 -> [ " from over here:\n\n"
, showSource src spots
, "\n\n"]
_ -> [ " from these spots, respectively:\n\n"
, showSource src spots
, "\n\n"]
styleAnnotated :: Annotated a => sty -> a -> Maybe (Range,sty)
styleAnnotated sty a = (,sty) <$> rangeForAnnotated a
mustBeType :: (Var v, Annotated a, Eq a) =>
[AT.Section Color.Style]
-> Env
-> String
-> a
-> a
-> Type.AnnotatedType v a
-> Type.AnnotatedType v a
-> [AT.Section Color.Style]
mustBeType initial env src expectedLoc mismatchSite expectedType mismatchedType =
initial ++
[ " Here, one is "
, AT.Text $ Color.type1 . renderType' env $ expectedType
, ", and the other is "
, AT.Text $ Color.type2 . renderType' env $ mismatchedType, ":\n\n"
, showSourceMaybes src [mismatchSiteS, expectedLocS]
, "\n"
] ++ fromOverHere' src [expectedTypeS, mismatchedTypeS]
[mismatchSiteS, expectedLocS]
where mismatchedTypeS = styleAnnotated Color.Type2 mismatchedType
mismatchSiteS = styleAnnotated Color.Type2 mismatchSite
expectedTypeS = styleAnnotated Color.Type1 expectedType
expectedLocS = styleAnnotated Color.Type1 expectedLoc
renderTypeError :: forall v a. (Var v, Annotated a, Ord a, Show a)
=> Env
@ -108,11 +163,11 @@ renderTypeError :: forall v a. (Var v, Annotated a, Ord a, Show a)
-> AT.AnnotatedDocument Color.Style
renderTypeError env e src = AT.AnnotatedDocument . Seq.fromList $ case e of
BooleanMismatch {..} ->
mustBeBool which env src mismatchSite mismatchedType
mustBeBool which env src mismatchSite foundType
++
[ "loc debug:"
, "\n mismatchSite: ", fromString $ annotatedToEnglish mismatchSite
, "\n mismatchedType: ", fromString $ annotatedToEnglish mismatchedType
, "\n mismatchSite: ", fromString $ annotatedToEnglish mismatchSite
, "\n foundType: ", fromString $ annotatedToEnglish foundType
, "\n"
]
++ summary note
@ -127,36 +182,59 @@ renderTypeError env e src = AT.AnnotatedDocument . Seq.fromList $ case e of
OrMismatch ->
[ "The arguments to ", AT.Text . Color.errorSite $ "or"
, " have to be"]
ExistentialMismatch {..} ->
mustBeType which env src expectedLoc mismatchSite expectedType foundType
++
[ "loc debug:"
, "\n mismatchSite: ", fromString $ annotatedToEnglish mismatchSite
, "\n foundType: ", fromString $ annotatedToEnglish foundType
, "\n expectedType: ", fromString $ annotatedToEnglish expectedType
, "\n"
]
++ summary note
where which =
case existentialMismatch of
IfBody ->
[ "The ", AT.Text . Color.errorSite $ "else"
, " clause of an ", AT.Text . Color.errorSite $ "if"
, " expression needs to have the same type as the "
, AT.Text . Color.errorSite $ "then", " clause.\n"]
VectorBody ->
[ "The elements of a vector all need to have the same type.\n"]
CaseBody ->
[ "Each case of a ", AT.Text . Color.errorSite $ "case"
, "/", AT.Text . Color.errorSite $ "of", " expression "
, "need to have the same type.\n"]
Mismatch {..} ->
[ (fromString . annotatedToEnglish) mismatchSite
, " has a type mismatch (", AT.Describe Color.ErrorSite, " below):\n\n"
, annotatedAsErrorSite src mismatchSite
, "\n"
, "The two types involved are:\n\n"
, " ", AT.Text $ styleInOverallType env overallType1 leaf1 Color.Type1
, " (", fromString (Char.toLower <$> annotatedToEnglish leaf1)
, " ", AT.Text $ styleInOverallType env foundType foundLeaf Color.Type1
, " (", fromString (Char.toLower <$> annotatedToEnglish foundLeaf)
, ", ", AT.Describe Color.Type1, ")\n"
, " ", AT.Text $ styleInOverallType env overallType2 leaf2 Color.Type2
, " (", fromString (Char.toLower <$> annotatedToEnglish leaf2)
, " ", AT.Text $ styleInOverallType env expectedType expectedLeaf Color.Type2
, " (", fromString (Char.toLower <$> annotatedToEnglish expectedLeaf)
, ", ", AT.Describe Color.Type2, ")\n"
, "\n"
-- , showSourceMaybes src
, AT.Blockquote . AT.markup (fromString src) . Set.fromList . catMaybes $
[ -- these are overwriting the colored ranges for some reason?
-- (,Color.ForceShow) <$> rangeForAnnotated mismatchSite
-- , (,Color.ForceShow) <$> rangeForType overallType1
-- , (,Color.ForceShow) <$> rangeForType overallType2
-- , (,Color.ForceShow) <$> rangeForType foundType
-- , (,Color.ForceShow) <$> rangeForType expectedType
-- ,
(,Color.Type1) <$> rangeForType leaf1
, (,Color.Type2) <$> rangeForType leaf2
(,Color.Type1) <$> rangeForType foundLeaf
, (,Color.Type2) <$> rangeForType expectedLeaf
]
, "\n"
, "loc debug:"
, "\n mismatchSite: ", fromString $ annotatedToEnglish mismatchSite
, "\n overallType1: ", fromString $ annotatedToEnglish overallType1
, "\n leaf1: ", fromString $ annotatedToEnglish leaf1
, "\n overallType2: ", fromString $ annotatedToEnglish overallType2
, "\n leaf2: ", fromString $ annotatedToEnglish leaf2
, "\n foundType: ", fromString $ annotatedToEnglish foundType
, "\n foundLeaf: ", fromString $ annotatedToEnglish foundLeaf
, "\n expectedType: ", fromString $ annotatedToEnglish expectedType
, "\n expectedLeaf: ", fromString $ annotatedToEnglish expectedLeaf
, "\n"
, "note debug:\n"
] ++ summary note
@ -236,7 +314,8 @@ renderTypeError env e src = AT.AnnotatedDocument . Seq.fromList $ case e of
["InSynthesizeApp t=", AT.Text $ renderType' env t
,", e=", renderTerm e]
C.InIfCond -> ["InIfCond"]
C.InIfBody -> ["InIfBody"]
C.InIfBody thenClause ->
["InIfBody thenClause=", fromString $ annotatedToEnglish thenClause]
C.InAndApp -> ["InAndApp"]
C.InOrApp -> ["InOrApp"]
-- ["InAndApp v=", AT.Text $ renderVar' env c v]
@ -419,18 +498,27 @@ typeErrorFromNote n@(C.Note (C.TypeMismatch ctx) path) =
-- replace any type vars with their solutions before returning
sub t = C.apply ctx t
in case (firstSubtype, lastSubtype, innermostTerm) of
(Just (leaf1, leaf2), Just (overall1, overall2), Just mismatchSite) ->
(Just (foundLeaf, expectedLeaf),
Just (foundType, expectedType),
Just mismatchSite) ->
let mismatchLoc = ABT.annotation mismatchSite in
if Ex.matchAny Ex.inAndApp n then
BooleanMismatch AndMismatch (ABT.annotation mismatchSite) overall1 n
BooleanMismatch AndMismatch (ABT.annotation mismatchSite) foundType n
else if Ex.matchAny Ex.inOrApp n then
BooleanMismatch OrMismatch (ABT.annotation mismatchSite) overall1 n
BooleanMismatch OrMismatch (ABT.annotation mismatchSite) foundType n
else if Ex.matchAny Ex.inIfCond n then
BooleanMismatch CondMismatch (ABT.annotation mismatchSite) overall1 n
BooleanMismatch CondMismatch (ABT.annotation mismatchSite) foundType n
else
Mismatch (sub overall1) (sub overall2)
(sub leaf1) (sub leaf2)
(ABT.annotation mismatchSite)
n
case Ex.matchMaybe Ex.inIfBody n of
Just expectedLoc ->
ExistentialMismatch IfBody expectedType expectedLoc
foundType mismatchLoc
n
Nothing ->
Mismatch (sub foundType) (sub expectedType)
(sub foundLeaf) (sub expectedLeaf)
(ABT.annotation mismatchSite)
n
_ -> Other n
typeErrorFromNote n@(C.Note (C.AbilityCheckFailure amb req _) _) =
let go :: C.Term v loc -> TypeError v loc

3
parser-typechecker/src/Unison/Term.hs
View File

@ -539,7 +539,8 @@ instance (Var v, Show p, Show a0, Show a) => Show (F v a0 p a) where
go _ (Int64 n) = (if n >= 0 then s "+" else s "") <> showsPrec 0 n
go _ (UInt64 n) = showsPrec 0 n
go _ (Float n) = showsPrec 0 n
go _ (Boolean b) = showsPrec 0 b
go _ (Boolean True) = s"true"
go _ (Boolean False) = s"false"
go p (Ann t k) = showParen (p > 1) $ showsPrec 0 t <> s":" <> showsPrec 0 k
go p (App f x) =
showParen (p > 9) $ showsPrec 9 f <> s" " <> showsPrec 10 x

4
parser-typechecker/src/Unison/Typechecker/Context.hs
View File

@ -110,7 +110,7 @@ data PathElement v loc
| InInstantiateR (Type v loc) v
| InSynthesizeApp (Type v loc) (Term v loc)
| InIfCond
| InIfBody
| InIfBody loc
| InAndApp
| InOrApp
deriving Show
@ -671,7 +671,7 @@ synthesize e = scope (InSynthesize e) $ do
generalizeExistentials ctx2 t <$ doRetract marker
go (Term.If' cond t f) = do
scope InIfCond $ check cond (Type.boolean l)
scope InIfBody $ foldM synthesizeApp (Type.iff2 l) [t, f]
scope (InIfBody $ ABT.annotation t) $ foldM synthesizeApp (Type.iff2 l) [t, f]
go (Term.And' a b) =
scope InAndApp $ foldM synthesizeApp (Type.andor' l) [a, b]
go (Term.Or' a b) =

32
parser-typechecker/src/Unison/Typechecker/Extractor.hs
View File

@ -1,9 +1,15 @@
{-# LANGUAGE LambdaCase #-}
module Unison.Typechecker.Extractor where
import Control.Monad
import Control.Applicative
import Data.Foldable (toList)
import Data.Monoid (First(..), getFirst)
-- import qualified Unison.ABT as ABT
-- import qualified Unison.Type as Type
-- import qualified Unison.TypeVar as TypeVar
import qualified Unison.Typechecker.Context as C
import Unison.Util.Monoid (whenM)
newtype NoteExtractor v loc a =
NoteExtractor { run :: C.Note v loc -> Maybe a }
@ -39,8 +45,34 @@ inIfCond :: C.PathElement v loc -> Bool
inIfCond C.InIfCond = True
inIfCond _ = False
inIfBody :: C.PathElement v loc -> Maybe loc
inIfBody (C.InIfBody loc) = Just loc
inIfBody _ = Nothing
-- inIfBody :: NoteExtractor v loc loc
-- inIfBody = do
-- (_, ()) <- adjacent inSynthesizeApp (fromPredicate inIfBody0)
-- NoteExtractor $ \_ ->
-- case t of
-- Type.Arrow' _i@(ABT.Var' vi) _o ->
-- Just (TypeVar.underlying vi, ABT.annotation e)
-- _ -> Nothing
inSynthesizeApp :: PathExtractor v loc (C.Type v loc, C.Term v loc)
inSynthesizeApp = PathExtractor $ \case
C.InSynthesizeApp t e -> Just (t,e)
_ -> Nothing
fromPredicate :: (C.PathElement v loc -> Bool) -> PathExtractor v loc ()
fromPredicate e = PathExtractor (\p -> whenM (e p) (pure ()))
matchAny :: (C.PathElement v loc -> Bool) -> C.Note v loc -> Bool
matchAny p = any p . toList . C.path
matchMaybe :: (C.PathElement v loc -> Maybe a) -> C.Note v loc -> Maybe a
matchMaybe p = getFirst . mconcat . fmap (First . p) . toList . C.path
-- App
-- = And
-- | Or

28
unison-src/errors/many-errors.u Normal file
View File

@ -0,0 +1,28 @@
id a = a
x = id 3
y = "Hello"
z = x
--or true x
--or true y
--or true 3
--f : Int64 -> Int64
--f = id
--or true (f 1)
--[1,2,3]
[x,y,3]
--foo : a -> a
--foo y = or y y
--if true then x else y
--if true then x else +3
--case 1 of
-- 3 | y -> "Hi"
-- 4 -> "bye"
--3 UInt64.+ 3.0
()