diff --git a/examples/non-examples/another-type-error.kl b/examples/non-examples/another-type-error.kl new file mode 100644 index 00000000..1ba29218 --- /dev/null +++ b/examples/non-examples/another-type-error.kl @@ -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)))))) + diff --git a/repl/Main.hs b/repl/Main.hs index d80849fc..72e485db 100644 --- a/repl/Main.hs +++ b/repl/Main.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BlockArguments #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -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 diff --git a/src/Expander.hs b/src/Expander.hs index c7c6686f..880b31e5 100644 --- a/src/Expander.hs +++ b/src/Expander.hs @@ -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 diff --git a/src/Expander/Error.hs b/src/Expander/Error.hs index 14e57306..6a9bca1b 100644 --- a/src/Expander/Error.hs +++ b/src/Expander/Error.hs @@ -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 @@ -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 @@ -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 @@ -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" diff --git a/src/Expander/Monad.hs b/src/Expander/Monad.hs index 69b74f24..cdf97e98 100644 --- a/src/Expander/Monad.hs +++ b/src/Expander/Monad.hs @@ -86,6 +86,9 @@ module Expander.Monad , stillStuck , schedule , scheduleType + -- * Type errors + , typeError + , withoutTypeErrors -- * Implementation parts , SyntacticCategory(..) , ExpansionEnv(..) @@ -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 @@ -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) @@ -313,6 +318,7 @@ initExpanderState = ExpanderState , _expanderCurrentDatatypes = Map.empty , _expanderCurrentConstructors = Map.empty , _expanderCurrentBindingTable = mempty + , _expanderCurrentTypeCheckErrors = mempty , _expanderExpressionTypes = Map.empty , _expanderCompletedSchemes = Map.empty , _expanderTypeStore = mempty @@ -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 @@ -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) diff --git a/src/Expander/Primitives.hs b/src/Expander/Primitives.hs index 2b8c7689..3ddf5741 100644 --- a/src/Expander/Primitives.hs +++ b/src/Expander/Primitives.hs @@ -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 @@ -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) @@ -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 @@ -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 diff --git a/src/Expander/TC.hs b/src/Expander/TC.hs index 1d62f2d9..32464d3f 100644 --- a/src/Expander/TC.hs +++ b/src/Expander/TC.hs @@ -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 @@ -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 () @@ -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') @@ -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 @@ -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')) diff --git a/src/Expander/Task.hs b/src/Expander/Task.hs index 5b68659c..c021d070 100644 --- a/src/Expander/Task.hs +++ b/src/Expander/Task.hs @@ -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 @@ -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 ++ ")" diff --git a/src/Syntax/SrcLoc.hs b/src/Syntax/SrcLoc.hs index 778eb66f..412d7a47 100644 --- a/src/Syntax/SrcLoc.hs +++ b/src/Syntax/SrcLoc.hs @@ -3,6 +3,7 @@ module Syntax.SrcLoc where import Control.Monad import Control.Lens +import Data.Ord (comparing) import Alpha import ShortShow @@ -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 @@ -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) diff --git a/tests/Test.hs b/tests/Test.hs index 07bf8f53..2b08924c 100644 --- a/tests/Test.hs +++ b/tests/Test.hs @@ -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) @@ -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 ) ]