Skip to content

Commit

Permalink
Fix: proper error handling for typechecker errors (#189)
Browse files Browse the repository at this point in the history 
* Fix: proper error handling for typechecker errors

* Improve error messages
  • Loading branch information
@jonaprieto
jonaprieto authored Jun 22, 2022
1 parent 9e817a6 commit a788478
Show file tree
Hide file tree
Showing 9 changed files with 229 additions and 62 deletions.
6 changes: 6 additions & 0 deletions src/MiniJuvix/Syntax/MicroJuvix/Error.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,9 @@ data TypeCheckerError
| ErrWrongType WrongType
| ErrUnsolvedMeta UnsolvedMeta
| ErrExpectedFunctionType ExpectedFunctionType
| ErrTooManyArgumentsIndType WrongNumberArgumentsIndType
| ErrTooFewArgumentsIndType WrongNumberArgumentsIndType
| ErrImpracticalPatternMatching ImpracticalPatternMatching

instance ToGenericError TypeCheckerError where
genericError :: TypeCheckerError -> GenericError
Expand All @@ -28,3 +31,6 @@ instance ToGenericError TypeCheckerError where
ErrWrongType e -> genericError e
ErrUnsolvedMeta e -> genericError e
ErrExpectedFunctionType e -> genericError e
ErrTooManyArgumentsIndType e -> genericError e
ErrTooFewArgumentsIndType e -> genericError e
ErrImpracticalPatternMatching e -> genericError e
163 changes: 121 additions & 42 deletions src/MiniJuvix/Syntax/MicroJuvix/Error/Types.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,18 @@ instance ToGenericError WrongConstructorType where
_genericErrorIntervals = [i]
}
where
i = getLoc (e ^. wrongCtorTypeName)
ctorName = e ^. wrongCtorTypeName
i = getLoc ctorName
msg =
"The constructor" <+> ppCode (e ^. wrongCtorTypeName) <+> "has type:"
<> line
<> indent' (ppCode (e ^. wrongCtorTypeActual))
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongCtorTypeExpected))
"The constructor"
<+> ppCode ctorName
<+> "has type:"
<> line
<> indent' (ppCode (e ^. wrongCtorTypeActual))
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongCtorTypeExpected))

data WrongReturnType = WrongReturnType
{ _wrongReturnTypeConstructorName :: Name,
Expand All @@ -53,15 +56,18 @@ instance ToGenericError WrongReturnType where
where
ctorName = e ^. wrongReturnTypeConstructorName
i = getLoc ctorName
j = getLoc (typeAsExpression (e ^. wrongReturnTypeActual))
ty = e ^. wrongReturnTypeActual
j = getLoc (typeAsExpression ty)
msg =
"The constructor" <+> ppCode ctorName <+> "has the wrong return type:"
<> line
<> indent' (ppCode (e ^. wrongReturnTypeActual))
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongReturnTypeExpected))
"The constructor"
<+> ppCode ctorName
<+> "has the wrong return type:"
<> line
<> indent' (ppCode ty)
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongReturnTypeExpected))

newtype UnsolvedMeta = UnsolvedMeta
{ _unsolvedMeta :: Hole
Expand Down Expand Up @@ -101,21 +107,27 @@ instance ToGenericError WrongConstructorAppArgs where
where
i = getLoc (e ^. wrongCtorAppApp . constrAppConstructor)
msg =
"The constructor:" <+> ctorName <+> "is being matched against" <+> numPats
<> ":"
<> line
<> indent' (ppCode (e ^. wrongCtorAppApp))
<> line
<> "but is expected to be matched against" <+> numTypes <+> "with the following types:"
<> line
<> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes))))
"The constructor:"
<+> ctorName
<+> "is being matched against"
<+> numPats
<> ":"
<> line
<> indent' (ppCode (e ^. wrongCtorAppApp))
<> line
<> "but is expected to be matched against"
<+> numTypes
<+> "with the following types:"
<> line
<> indent' (hsep (ctorName : (ppCode <$> (e ^. wrongCtorAppTypes))))
numPats :: Doc ann
numPats = pat (length (e ^. wrongCtorAppApp . constrAppParameters))
numTypes :: Doc ann
numTypes = pat (length (e ^. wrongCtorAppTypes))

ctorName :: Doc Eann
ctorName = ppCode (e ^. wrongCtorAppApp . constrAppConstructor)

pat :: Int -> Doc ann
pat n = pretty n <+> plural "pattern" "patterns" n

Expand All @@ -138,15 +150,19 @@ instance ToGenericError WrongType where
where
i = getLoc (e ^. wrongTypeExpression)
msg =
"Type error near" <+> pretty (getLoc subjectExpr) <> "."
<> line
<> "The expression" <+> ppCode subjectExpr <+> "has type:"
<> line
<> indent' (ppCode (e ^. wrongTypeInferredType))
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongTypeExpectedType))
"Type error near"
<+> pretty (getLoc subjectExpr)
<> "."
<> line
<> "The expression"
<+> ppCode subjectExpr
<+> "has type:"
<> line
<> indent' (ppCode (e ^. wrongTypeInferredType))
<> line
<> "but is expected to have type:"
<> line
<> indent' (ppCode (e ^. wrongTypeExpectedType))

subjectExpr :: Expression
subjectExpr = e ^. wrongTypeExpression
Expand All @@ -171,14 +187,77 @@ instance ToGenericError ExpectedFunctionType where
where
i = getLoc (e ^. expectedFunctionTypeExpression)
msg =
"Type error near" <+> pretty (getLoc subjectExpr) <> "."
<> line
<> "In the expression:"
<> line
<> indent' (ppCode (e ^. expectedFunctionTypeExpression))
<> line
<> "the expression" <+> ppCode (e ^. expectedFunctionTypeApp) <+> "is expected to have a function type but has type:"
<> line
<> indent' (ppCode (e ^. expectedFunctionTypeType))
"Type error near"
<+> pretty (getLoc subjectExpr)
<> "."
<> line
<> "In the expression:"
<> line
<> indent' (ppCode (e ^. expectedFunctionTypeExpression))
<> line
<> "the expression"
<+> ppCode (e ^. expectedFunctionTypeApp)
<+> "is expected to have a function type but has type:"
<> line
<> indent' (ppCode (e ^. expectedFunctionTypeType))
subjectExpr :: Expression
subjectExpr = e ^. expectedFunctionTypeExpression

data WrongNumberArgumentsIndType = WrongNumberArgumentsIndType
{ _wrongNumberArgumentsIndTypeActualType :: Type,
_wrongNumberArgumentsIndTypeExpectedNumArgs :: Int,
_wrongNumberArgumentsIndTypeActualNumArgs :: Int
}

makeLenses ''WrongNumberArgumentsIndType

instance ToGenericError WrongNumberArgumentsIndType where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
ty = e ^. wrongNumberArgumentsIndTypeActualType
i = getLoc (typeAsExpression ty)
expectedNumArgs = e ^. wrongNumberArgumentsIndTypeExpectedNumArgs
actualNumArgs = e ^. wrongNumberArgumentsIndTypeActualNumArgs
msg =
"The type"
<+> pretty (getTypeName ty)
<+> "expects"
<+> ( if
| expectedNumArgs == 0 -> "no arguments"
| expectedNumArgs == 1 -> "one argument"
| otherwise -> pretty expectedNumArgs <+> "arguments"
)
<> ", but"
<+> ( if
| actualNumArgs == 0 -> "no argument is"
| actualNumArgs == 1 -> "only one argument is"
| otherwise -> pretty actualNumArgs <+> "arguments are"
)
<+> "given"

newtype ImpracticalPatternMatching = ImpracticalPatternMatching
{ _impracticalPatternMatchingType :: Type
}

makeLenses ''ImpracticalPatternMatching

instance ToGenericError ImpracticalPatternMatching where
genericError e =
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = prettyError msg,
_genericErrorIntervals = [i]
}
where
ty = e ^. impracticalPatternMatchingType
i = getLoc (typeAsExpression ty)
msg =
"The type"
<+> ppCode ty
<+> "is not an inductive data type."
<+> "Therefore, pattern-matching is not available here"
16 changes: 11 additions & 5 deletions src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -429,11 +429,11 @@ unfoldApplication = fmap (fmap snd) . unfoldApplication'

unfoldTypeApplication :: TypeApplication -> (Type, NonEmpty Type)
unfoldTypeApplication (TypeApplication l' r' _) = second (|: r') (unfoldType l')
where
unfoldType :: Type -> (Type, [Type])
unfoldType t = case t of
TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
_ -> (t, [])

unfoldType :: Type -> (Type, [Type])
unfoldType = \case
TypeApp (TypeApplication l r _) -> second (`snoc` r) (unfoldType l)
t -> (t, [])

foldTypeApp :: Type -> [Type] -> Type
foldTypeApp ty = \case
Expand All @@ -445,3 +445,9 @@ foldTypeAppName tyName indParams =
foldTypeApp
(TypeIden (TypeIdenInductive tyName))
(map (TypeIden . TypeIdenVariable) indParams)

getTypeName :: Type -> Maybe Name
getTypeName = \case
(TypeIden (TypeIdenInductive tyName)) -> Just tyName
(TypeApp (TypeApplication l _ _)) -> getTypeName l
_ -> Nothing
32 changes: 27 additions & 5 deletions src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -237,15 +237,37 @@ checkPattern funName = go
)
)
checkSaturatedInductive :: Type -> Sem r (InductiveName, [(InductiveParameter, Type)])
checkSaturatedInductive t = do
(ind, args) <- viewInductiveApp t
checkSaturatedInductive ty = do
(ind, args) <- viewInductiveApp ty
params <-
(^. inductiveInfoDef . inductiveParameters)
<$> lookupInductive ind
let numArgs = length args
numParams = length params
when (numArgs < numParams) (error "unsaturated inductive type")
when (numArgs > numParams) (error "too many arguments to inductive type")
when
(numArgs < numParams)
( throw
( ErrTooFewArgumentsIndType
( WrongNumberArgumentsIndType
{ _wrongNumberArgumentsIndTypeActualType = ty,
_wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
_wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
}
)
)
)
when
(numArgs > numParams)
( throw
( ErrTooManyArgumentsIndType
( WrongNumberArgumentsIndType
{ _wrongNumberArgumentsIndTypeActualType = ty,
_wrongNumberArgumentsIndTypeActualNumArgs = numArgs,
_wrongNumberArgumentsIndTypeExpectedNumArgs = numParams
}
)
)
)
return (ind, zip params args)

freshHole :: Members '[Inference, NameIdGen] r => Interval -> Sem r Hole
Expand Down Expand Up @@ -393,7 +415,7 @@ viewInductiveApp ::
Sem r (InductiveName, [Type])
viewInductiveApp ty = case t of
TypeIden (TypeIdenInductive n) -> return (n, as)
_ -> throw @TypeCheckerError (error "only inductive types can be pattern matched")
_ -> throw (ErrImpracticalPatternMatching (ImpracticalPatternMatching ty))
where
(t, as) = viewTypeApp ty

Expand Down
45 changes: 39 additions & 6 deletions src/MiniJuvix/Translation/AbstractToMicroJuvix.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -278,33 +278,66 @@ goInductiveDef i = case i ^. Abstract.inductiveType of
Just {} -> unsupported "inductive indices"
_ -> helper
where
indTypeName = i ^. Abstract.inductiveName
helper = do
inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
let indTy :: Type = foldTypeAppName indTypeName (map (^. inductiveParamName) inductiveParameters')
inductiveConstructors' <- mapM (goConstructorDef indTy) (i ^. Abstract.inductiveConstructors)
let indTypeName = i ^. Abstract.inductiveName
indParamNames = map (^. inductiveParamName) inductiveParameters'
inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors)
return
InductiveDef
{ _inductiveName = indTypeName,
_inductiveParameters = inductiveParameters',
_inductiveConstructors = inductiveConstructors'
}
where
goConstructorDef :: Type -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
goConstructorDef expectedReturnType c = do
goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
goConstructorDef expectedTypeName expectedNameParms c = do
(_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
let ctorName = c ^. Abstract.constructorName
expectedReturnType :: Type
expectedReturnType = foldTypeAppName expectedTypeName expectedNameParms
expectedNumArgs = length expectedNameParms
(_, actualReturnTypeParams) = unfoldType actualReturnType
actualNumArgs = length actualReturnTypeParams
sameTypeName = Just expectedTypeName == getTypeName actualReturnType
if
| actualReturnType == expectedReturnType ->
return
InductiveConstructorDef
{ _constructorName = ctorName,
_constructorParameters = _constructorParameters'
}
| sameTypeName,
actualNumArgs < expectedNumArgs ->
throw
( ErrTooFewArgumentsIndType
( WrongNumberArgumentsIndType
{ _wrongNumberArgumentsIndTypeActualType = actualReturnType,
_wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
_wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
}
)
)
| sameTypeName,
actualNumArgs > expectedNumArgs ->
throw
( ErrTooManyArgumentsIndType
( WrongNumberArgumentsIndType
{ _wrongNumberArgumentsIndTypeActualType = actualReturnType,
_wrongNumberArgumentsIndTypeActualNumArgs = actualNumArgs,
_wrongNumberArgumentsIndTypeExpectedNumArgs = expectedNumArgs
}
)
)
| otherwise ->
throw
( ErrWrongReturnType
(WrongReturnType ctorName expectedReturnType actualReturnType)
( WrongReturnType
{ _wrongReturnTypeConstructorName = ctorName,
_wrongReturnTypeExpected = expectedReturnType,
_wrongReturnTypeActual = actualReturnType
}
)
)

goTypeApplication :: Abstract.Application -> Sem r TypeApplication
Expand Down
13 changes: 10 additions & 3 deletions test/TypeCheck/Negative.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,17 @@ tests =
ErrWrongReturnType {} -> Nothing
_ -> wrongError,
NegTest
"Wrong return type for a constructor of a data type with parameters "
"Too few arguments for the return type of a constructor"
"MicroJuvix"
"WrongReturnTypeParameters.mjuvix"
"WrongReturnTypeTooFewArguments.mjuvix"
$ \case
ErrWrongReturnType {} -> Nothing
ErrTooFewArgumentsIndType {} -> Nothing
_ -> wrongError,
NegTest
"Too many arguments for the return type of a constructor"
"MicroJuvix"
"WrongReturnTypeTooManyArguments.mjuvix"
$ \case
ErrTooManyArgumentsIndType {} -> Nothing
_ -> wrongError
]
Loading

0 comments on commit a788478

Please sign in to comment.