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

Fix for crash with wildcard used in type definition #2405

Merged
merged 5 commits into from
Oct 2, 2023
Merged
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
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ data ScoperError
| ErrIncomparablePrecedences IncomaprablePrecedences
| ErrAliasCycle AliasCycle
| ErrInvalidRangeNumber InvalidRangeNumber
| ErrUnsupported Unsupported

instance ToGenericError ScoperError where
genericError = \case
Expand Down Expand Up @@ -91,3 +92,4 @@ instance ToGenericError ScoperError where
ErrIncomparablePrecedences e -> genericError e
ErrAliasCycle e -> genericError e
ErrInvalidRangeNumber e -> genericError e
ErrUnsupported e -> genericError e
Original file line number Diff line number Diff line change
Expand Up @@ -929,3 +929,21 @@ instance ToGenericError AliasCycle where
where
i :: Interval
i = getLoc _aliasCycleDef

data Unsupported = Unsupported
{ _unsupportedMsg :: Text,
_unsupportedLoc :: Interval
}
deriving stock (Show)

instance ToGenericError Unsupported where
genericError Unsupported {..} = do
return
GenericError
{ _genericErrorLoc = i,
_genericErrorMessage = mkAnsiText _unsupportedMsg,
_genericErrorIntervals = [i]
}
where
i :: Interval
i = _unsupportedLoc
12 changes: 8 additions & 4 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,9 +39,6 @@ type MCache = Cache Concrete.ModuleIndex Internal.Module
-- | Needed to generate field projections.
type ConstructorInfos = HashMap Internal.ConstructorName ConstructorInfo

unsupported :: Text -> a
unsupported msg = error $ msg <> "Scoped to Internal: not yet supported"

fromConcrete ::
(Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen, Termination] r) =>
Scoper.ScoperResult ->
Expand Down Expand Up @@ -537,7 +534,14 @@ goInductiveParameters params@InductiveParameters {..} = do
paramType' <- goRhs _inductiveParametersRhs
case paramType' of
Internal.ExpressionUniverse {} -> return ()
_ -> unsupported "only type variables of small types are allowed"
Internal.ExpressionHole {} -> return ()
_ ->
throw $
ErrUnsupported
Unsupported
{ _unsupportedMsg = "only type variables of small types are allowed",
_unsupportedLoc = getLoc params
}

let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter
goInductiveParameter var =
Expand Down
7 changes: 7 additions & 0 deletions test/Scope/Negative.hs
Original file line number Diff line number Diff line change
Expand Up @@ -350,5 +350,12 @@ scoperErrorTests =
$(mkRelFile "DanglingDoubleBrace.juvix")
$ \case
ErrDanglingDoubleBrace {} -> Nothing
_ -> wrongError,
NegTest
"Unsupported type"
$(mkRelDir ".")
$(mkRelFile "UnsupportedType.juvix")
$ \case
ErrUnsupported {} -> Nothing
_ -> wrongError
]
6 changes: 5 additions & 1 deletion test/Typecheck/Positive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,11 @@ tests =
posTest
"Hole as numeric type"
$(mkRelDir "issue2373")
$(mkRelFile "Main.juvix")
$(mkRelFile "Main.juvix"),
posTest
"Hole in type parameter"
$(mkRelDir ".")
$(mkRelFile "HoleTypeParameter.juvix")
]
<> [ compilationTest t | t <- Compilation.tests
]
5 changes: 5 additions & 0 deletions tests/negative/UnsupportedType.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module UnsupportedType;

type List' (A : Type -> Type) :=
| nil'
| cons' A (List' A);
5 changes: 5 additions & 0 deletions tests/positive/HoleTypeParameter.juvix
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module HoleTypeParameter;

type List' (A : _) :=
| nil'
| cons' A (List' A);