Implement wildcard constructor (#2550)

- Closes #2549 

The implementation of wildcard constructors was previously done in the
arity checker. I did not realise I was missing it because there was not
tests for it that included typechecking (we were only checking
formatting).

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs

@@ -731,10 +731,23 @@ checkPattern = go
       whenJust name (\n -> addPatternVar n ty (argTy ^. paramName))
       pat' <- case pat of
         PatternVariable v -> addPatternVar v ty (argTy ^. paramName) $> pat
-        PatternWildcardConstructor {} -> impossible
+        PatternWildcardConstructor c -> checkWildcardConstructor pat ty c
         PatternConstructorApp a -> goPatternConstructor pat ty a
       return (set patternArgPattern pat' patArg)
       where
+        checkWildcardConstructor :: Pattern -> Expression -> WildcardConstructor -> Sem r Pattern
+        checkWildcardConstructor pat ty w = do
+          let c = w ^. wildcardConstructor
+          numArgs <- length . constructorArgs . (^. constructorInfoType) <$> lookupConstructor c
+          holeArgs <- replicateM numArgs (genWildcard (getLoc w) Explicit)
+          let capp =
+                ConstructorApp
+                  { _constrAppConstructor = c,
+                    _constrAppParameters = holeArgs,
+                    _constrAppType = Nothing
+                  }
+          goPatternConstructor pat ty capp
+
         goPatternConstructor :: Pattern -> Expression -> ConstructorApp -> Sem r Pattern
         goPatternConstructor pat ty a = do
           s <- checkSaturatedInductive ty

test/Typecheck/Positive.hs

@@ -315,6 +315,10 @@ tests =
       "Import a .juvix.md module in a .juvix.md file"
       $(mkRelDir "MarkdownImport")
       $(mkRelFile "C.juvix.md"),
+    posTest
+      "Typecheck constructor wildcard"
+      $(mkRelDir ".")
+      $(mkRelFile "ConstructorWildcard.juvix"),
     posTestAbsDir
       "Typecheck orphan file"
       (relToProject $(mkRelDir "tests/WithoutPackageFile"))

tests/positive/ConstructorWildcard.juvix

@@ -0,0 +1,16 @@
+module ConstructorWildcard;
+
+type Bool :=
+ false | true;
+
+type either (A B : Type) :=
+  left A
+  | right B;
+
+isLeft {A B} : either A B → Bool
+ | left@{} := true
+ | right@{} := false;
+
+not : Bool → Bool
+ | false@{} := true
+ | true := false;