Skip to content
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.

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

WIP: Type error display improvements #49

Draft
wants to merge 6 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
17 changes: 17 additions & 0 deletions examples/non-examples/another-type-error.kl
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
#lang kernel



(datatype (Wrap A) (wrap A))
(datatype (Both A) (both A A))
(datatype (Throth A) (throth A A A))

(example (let (x (wrap (wrap (wrap (wrap (wrap (wrap 'foo)))))))
(let (f (lambda (x) (lambda (y) (both x y))))
((f x) (wrap 'bar)))))


(example (let (x (wrap (wrap (wrap (wrap (wrap (wrap 'foo)))))))
(let (f (lambda (x) (lambda (y) (lambda (z) (throth x y z)))))
(((f x) (wrap 'bar)) (wrap (wrap 'spinach))))))

3 changes: 2 additions & 1 deletion repl/Main.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
Expand Down Expand Up @@ -95,7 +96,7 @@ mainWithOptions opts =
mn <- moduleNameFromPath file
ctx <- mkInitContext mn
void $ execExpand ctx initializeKernel
st <- execExpand ctx $ completely $ do
st <- execExpand ctx $ completely do
visit mn
getState
case st of
Expand Down
11 changes: 0 additions & 11 deletions src/Expander.hs
Original file line number Diff line number Diff line change
Expand Up @@ -729,17 +729,6 @@ runTask (tid, localData, task) = withLocal localData $ do
ValueMacroAction macroAction -> do
forkInterpretMacroAction dest macroAction kont
other -> expandEval $ evalErrorType "macro action" other
EvalDefnAction x n p expr ->
linkedCore expr >>=
\case
Nothing -> stillStuck tid task
Just definiens ->
inPhase p $ do
val <- expandEval (eval definiens)
modifyState $ over (expanderCurrentEnvs . at p) $
\case
Nothing -> Just $ Env.singleton x n val
Just env -> Just $ env <> Env.singleton x n val
GeneralizeType edest ty schdest -> do
ready <- isExprChecked edest
if ready
Expand Down
74 changes: 56 additions & 18 deletions src/Expander/Error.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ module Expander.Error where

import Control.Lens
import Numeric.Natural
import Data.List (sortBy)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Text (Text)
import qualified Data.Text as T

Expand Down Expand Up @@ -46,13 +48,19 @@ data ExpansionErr
| ReaderError Text
| WrongMacroContext Syntax MacroContext MacroContext
| NotValidType Syntax
| TypeMismatch (Maybe SrcLoc) Ty Ty
| OccursCheckFailed MetaPtr Ty
| TypeCheckErrors (NonEmpty TypeCheckError)
| WrongArgCount Syntax Constructor Int Int
| NotAConstructor Syntax
| WrongDatatypeArity Syntax Datatype Natural Int
deriving (Show)

data TypeCheckError
= TypeMismatch (Maybe SrcLoc) Ty Ty (Maybe (Ty, Ty))
-- ^ Blame for constraint, expected, got, and specific part that doesn't match
| OccursCheckFailed MetaPtr Ty
deriving (Show)


data MacroContext
= ExpressionCtx
| TypeCtx
Expand Down Expand Up @@ -150,23 +158,22 @@ instance Pretty VarInfo ExpansionErr where
]
pp env (NotValidType stx) =
hang 2 $ group $ vsep [text "Not a type:", pp env stx]
pp env (TypeMismatch loc expected got) =
group $ vsep [ group $ hang 2 $ vsep [ text "Type mismatch at"
, maybe (text "unknown location") (pp env) loc <> text "."
]
, group $ vsep [ group $ hang 2 $ vsep [ text "Expected"
, pp env expected
]
, group $ hang 2 $ vsep [ text "but got"
, pp env got
]
]
]

pp env (OccursCheckFailed ptr ty) =
hang 2 $ group $ vsep [ text "Occurs check failed:"
, group (vsep [viaShow ptr, "≠", pp env ty])
]
pp env (TypeCheckErrors (err :| [])) = pp env err

pp env (TypeCheckErrors (err :| errs)) =
hang 2 $ vsep [ text "Type errors:"
, vsep (map (bulleted . pp env) (sortBy typeErrOrder (err : errs)))
]
where
bulleted doc = text " • " <> align doc
typeErrOrder :: TypeCheckError -> TypeCheckError -> Ordering
typeErrOrder (TypeMismatch loc1 _ _ _) (TypeMismatch loc2 _ _ _) =
loc1 `compare` loc2
typeErrOrder (TypeMismatch _ _ _ _) (OccursCheckFailed _ _) = GT
typeErrOrder (OccursCheckFailed _ _) (TypeMismatch _ _ _ _) = LT
typeErrOrder (OccursCheckFailed _ _) (OccursCheckFailed _ _) = EQ

pp env (WrongArgCount stx ctor wanted got) =
hang 2 $
vsep [ text "Wrong number of arguments for constructor" <+> pp env ctor
Expand All @@ -183,6 +190,37 @@ instance Pretty VarInfo ExpansionErr where
, text "In" <+> align (pp env stx)
]


instance Pretty VarInfo TypeCheckError where
pp env (TypeMismatch loc expected got specifically) =
group $ vsep [ group $ hang 2 $ vsep [ text "Type mismatch at"
, maybe (text "unknown location") (pp env) loc <> text ":"
]
, group $ vsep $
[ group $ hang 2 $ vsep [ text "Expected"
, pp env expected
]
, group $ hang 2 $ vsep [ text "but got"
, pp env got
]
] ++
case specifically of
Nothing -> []
Just (expected', got') ->
[ hang 2 $ group $ vsep [text "Specifically,"
, group (vsep [ pp env expected'
, text "doesn't match" <+> pp env got'
])
]
]
]

pp env (OccursCheckFailed ptr ty) =
hang 2 $ group $ vsep [ text "Occurs check failed:"
, group (vsep [viaShow ptr, "≠", pp env ty])
]


instance Pretty VarInfo MacroContext where
pp _env ExpressionCtx = text "an expression"
pp _env ModuleCtx = text "a module"
Expand Down
25 changes: 24 additions & 1 deletion src/Expander/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,9 @@ module Expander.Monad
, stillStuck
, schedule
, scheduleType
-- * Type errors
, typeError
, withoutTypeErrors
-- * Implementation parts
, SyntacticCategory(..)
, ExpansionEnv(..)
Expand Down Expand Up @@ -142,6 +145,7 @@ import Control.Monad.Except
import Control.Monad.Reader
import Data.Foldable
import Data.IORef
import Data.List.NonEmpty (NonEmpty(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
Expand Down Expand Up @@ -277,6 +281,7 @@ data ExpanderState = ExpanderState
, _expanderCurrentDatatypes :: !(Map Phase (Map Datatype DatatypeInfo))
, _expanderCurrentConstructors :: !(Map Phase (Map Constructor (ConstructorInfo Ty)))
, _expanderCurrentBindingTable :: !BindingTable
, _expanderCurrentTypeCheckErrors :: [TypeCheckError]
, _expanderExpressionTypes :: !(Map SplitCorePtr Ty)
, _expanderCompletedSchemes :: !(Map SchemePtr (Scheme Ty))
, _expanderTypeStore :: !(TypeStore Ty)
Expand Down Expand Up @@ -313,6 +318,7 @@ initExpanderState = ExpanderState
, _expanderCurrentDatatypes = Map.empty
, _expanderCurrentConstructors = Map.empty
, _expanderCurrentBindingTable = mempty
, _expanderCurrentTypeCheckErrors = mempty
, _expanderExpressionTypes = Map.empty
, _expanderCompletedSchemes = Map.empty
, _expanderTypeStore = mempty
Expand Down Expand Up @@ -777,7 +783,7 @@ kernelExports :: Expand Exports
kernelExports = view expanderKernelExports <$> getState

completely :: Expand a -> Expand a
completely body = do
completely body = withoutTypeErrors do
oldTasks <- getTasks
clearTasks
a <- body
Expand Down Expand Up @@ -827,3 +833,20 @@ scheduleType stx = do
dest <- liftIO newSplitTypePtr
forkExpandType dest stx
return dest

typeError :: TypeCheckError -> Expand ()
typeError err =
modifyState $ over expanderCurrentTypeCheckErrors (err:)

withoutTypeErrors :: Expand a -> Expand a
withoutTypeErrors act = do
x <- act
noTypeErrors
pure x

where
noTypeErrors = do
errs <- view expanderCurrentTypeCheckErrors <$> getState
case errs of
[] -> pure ()
(e:es) -> throwError $ TypeCheckErrors (e :| es)
8 changes: 5 additions & 3 deletions src/Expander/Primitives.hs
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ defineMacros dest outScopesDest stx = do
b <- freshBinding
addDefinedBinding theName b
macroDest <- inEarlierPhase $
schedule (Ty (TFun (Ty TSyntax) (Ty (TMacro (Ty TSyntax)))))
schedule typeOfMacro
(addScope p mdef sc)
v <- freshMacroVar
bind b $ EIncompleteMacro v theName macroDest
Expand Down Expand Up @@ -416,7 +416,7 @@ letSyntax t dest stx = do
v <- freshMacroVar
macroDest <- inEarlierPhase $ do
psc <- phaseRoot
schedule (Ty (TFun (Ty TSyntax) (Ty (TMacro (Ty TSyntax)))))
schedule typeOfMacro
(addScope (prior p) mdef psc)
forkAwaitingMacro b v m' macroDest (ExprDest t dest) (addScope p body sc)

Expand Down Expand Up @@ -596,7 +596,6 @@ varPrepHelper varStx = do
addLocalBinding x' b
return (sc, x', b)


prepareVar :: Syntax -> Expand (Scope, Ident, Var)
prepareVar varStx = do
(sc, x', b) <- varPrepHelper varStx
Expand All @@ -611,3 +610,6 @@ primitiveDatatype name args =
}
in Ty $ TDatatype dt args

-- | The type of user-written macros: Syntax -> Macro Syntax
typeOfMacro :: Ty
typeOfMacro = Ty $ TFun (Ty TSyntax) $ Ty $ TMacro $ Ty TSyntax
29 changes: 20 additions & 9 deletions src/Expander/TC.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ViewPatterns #-}
module Expander.TC where
module Expander.TC (unify, freshMeta, inst, specialize, varType, makeTypeMetas, generalizeType) where

import Control.Lens hiding (indices)
import Control.Monad.Except
Expand Down Expand Up @@ -73,7 +73,7 @@ occursCheck ptr t = do
if ptr `elem` free
then do
t' <- normAll t
throwError $ OccursCheckFailed ptr t'
typeError $ OccursCheckFailed ptr t'
else pure ()

pruneLevel :: Traversable f => BindingLevel -> f MetaPtr -> Expand ()
Expand Down Expand Up @@ -192,9 +192,12 @@ instance UnificationErrorBlame SrcLoc where
instance UnificationErrorBlame SplitCorePtr where
getBlameLoc ptr = view (expanderOriginLocations . at ptr) <$> getState

-- The expected type is first, the received is second
unify :: UnificationErrorBlame blame => blame -> Ty -> Ty -> Expand ()
unify blame t1 t2 = do
unify loc t1 t2 = unifyWithBlame (loc, t1, t2) 0 t1 t2

-- The expected type is first, the received is second
unifyWithBlame :: UnificationErrorBlame blame => (blame, Ty, Ty) -> Natural -> Ty -> Ty -> Expand ()
unifyWithBlame blame depth t1 t2 = do
t1' <- normType t1
t2' <- normType t2
unify' (unTy t1') (unTy t2')
Expand All @@ -204,10 +207,10 @@ unify blame t1 t2 = do
-- Rigid-rigid
unify' TSyntax TSyntax = pure ()
unify' TSignal TSignal = pure ()
unify' (TFun a c) (TFun b d) = unify blame b a >> unify blame c d
unify' (TMacro a) (TMacro b) = unify blame a b
unify' (TFun a c) (TFun b d) = unifyWithBlame blame (depth + 1) b a >> unifyWithBlame blame (depth + 1) c d
unify' (TMacro a) (TMacro b) = unifyWithBlame blame (depth + 1) a b
unify' (TDatatype dt1 args1) (TDatatype dt2 args2)
| dt1 == dt2 = traverse_ (uncurry (unify blame)) (zip args1 args2)
| dt1 == dt2 = traverse_ (uncurry (unifyWithBlame blame (depth + 1))) (zip args1 args2)

-- Flex-flex
unify' (TMetaVar ptr1) (TMetaVar ptr2) = do
Expand All @@ -223,5 +226,13 @@ unify blame t1 t2 = do

-- Mismatch
unify' expected received = do
loc <- getBlameLoc blame
throwError $ TypeMismatch loc (Ty expected) (Ty received)
let (here, outerExpected, outerReceived) = blame
loc <- getBlameLoc here
e' <- normAll $ Ty expected
r' <- normAll $ Ty received
if depth == 0
then typeError $ TypeMismatch loc e' r' Nothing
else do
outerE' <- normAll outerExpected
outerR' <- normAll outerReceived
typeError $ TypeMismatch loc outerE' outerR' (Just (e', r'))
2 changes: 0 additions & 2 deletions src/Expander/Task.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,6 @@ data ExpanderTask
-- Syntax's remaining declaration forms.
| InterpretMacroAction MacroDest MacroAction [Closure]
| ContinueMacroAction MacroDest Value [Closure]
| EvalDefnAction Var Ident Phase SplitCorePtr
| GeneralizeType SplitCorePtr Ty SchemePtr
-- ^ The expression whose type should be generalized, and the place to put the resulting scheme
| ExpandVar Ty SplitCorePtr Syntax Var
Expand Down Expand Up @@ -95,7 +94,6 @@ instance ShortShow ExpanderTask where
shortShow (ExpandDeclForms _dest _scs waitingOn outScopesDest stx) = "(ExpandDeclForms _ " ++ show waitingOn ++ " " ++ show outScopesDest ++ " " ++ T.unpack (syntaxText stx) ++ ")"
shortShow (InterpretMacroAction _dest act kont) = "(InterpretMacroAction " ++ show act ++ " " ++ show kont ++ ")"
shortShow (ContinueMacroAction _dest value kont) = "(ContinueMacroAction " ++ show value ++ " " ++ show kont ++ ")"
shortShow (EvalDefnAction var name phase _expr) = "(EvalDefnAction " ++ show var ++ " " ++ shortShow name ++ " " ++ show phase ++ ")"
shortShow (GeneralizeType e _ _) = "(GeneralizeType " ++ show e ++ " _ _)"
shortShow (ExpandVar t d x v) = "(ExpandVar " ++ show t ++ " " ++ show d ++ " " ++ show x ++ " " ++ show v ++ ")"
shortShow (EstablishConstructors _ _ dt _) = "(EstablishConstructors " ++ show dt ++ ")"
Expand Down
16 changes: 16 additions & 0 deletions src/Syntax/SrcLoc.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module Syntax.SrcLoc where

import Control.Monad
import Control.Lens
import Data.Ord (comparing)

import Alpha
import ShortShow
Expand All @@ -14,6 +15,14 @@ data SrcPos = SrcPos
deriving (Eq, Show)
makeLenses ''SrcPos

-- This is the derived instance, but because it's used in things like
-- error messages rather than just in things like Map keys, we write
-- it explicitly
instance Ord SrcPos where
compare =
comparing (view srcPosLine) <>
comparing (view srcPosCol)

instance ShortShow SrcPos where
shortShow (SrcPos l c) = show l ++ "." ++ show c

Expand All @@ -25,6 +34,13 @@ data SrcLoc = SrcLoc
deriving (Eq, Show)
makeLenses ''SrcLoc

instance Ord SrcLoc where
compare loc1 loc2 =
comparing (view srcLocFilePath) loc1 loc2 <>
comparing (view srcLocStart) loc1 loc2 <>
-- NB They are flipped so that shorter (more specific) locations come before others
comparing (view srcLocEnd) loc2 loc1

instance AlphaEq SrcLoc where
alphaCheck x y = guard (x == y)

Expand Down
3 changes: 2 additions & 1 deletion tests/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ module Main where

import Control.Lens hiding (List)
import Control.Monad
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Map as Map
import Control.Monad.IO.Class (liftIO)
import Data.Maybe (maybeToList)
Expand Down Expand Up @@ -451,7 +452,7 @@ moduleTests = testGroup "Module tests" [ shouldWork, shouldn'tWork ]
)
, ( "examples/non-examples/type-errors.kl"
, \case
TypeMismatch (Just _) _ _ -> True
TypeCheckErrors ((TypeMismatch (Just _) _ _ _) :| _) -> True
_ -> False
)
]
Expand Down