Fix for crash with wildcard used in type definition (#2405)

- Closes #2292.

Holes are now allowed in the type of inductive parameters.
If the type is unsupported, a user error is thrown.

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs

@@ -50,6 +50,7 @@ data ScoperError
   | ErrIncomparablePrecedences IncomaprablePrecedences
   | ErrAliasCycle AliasCycle
   | ErrInvalidRangeNumber InvalidRangeNumber
+  | ErrUnsupported Unsupported
 
 instance ToGenericError ScoperError where
   genericError = \case
@@ -91,3 +92,4 @@ instance ToGenericError ScoperError where
     ErrIncomparablePrecedences e -> genericError e
     ErrAliasCycle e -> genericError e
     ErrInvalidRangeNumber e -> genericError e
+    ErrUnsupported e -> genericError e

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs

@@ -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

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -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 ->
@@ -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 =

test/Scope/Negative.hs

@@ -350,5 +350,12 @@ scoperErrorTests =
       $(mkRelFile "DanglingDoubleBrace.juvix")
       $ \case
         ErrDanglingDoubleBrace {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Unsupported type"
+      $(mkRelDir ".")
+      $(mkRelFile "UnsupportedType.juvix")
+      $ \case
+        ErrUnsupported {} -> Nothing
         _ -> wrongError
   ]

test/Typecheck/Positive.hs

@@ -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
        ]

tests/negative/UnsupportedType.juvix

@@ -0,0 +1,5 @@
+module UnsupportedType;
+
+type List' (A : Type -> Type) :=
+  | nil'
+  | cons' A (List' A);

tests/positive/HoleTypeParameter.juvix

@@ -0,0 +1,5 @@
+module HoleTypeParameter;
+
+type List' (A : _) :=
+  | nil'
+  | cons' A (List' A);