diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 7edaa3551f..29b6551470 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/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 diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index e030efbf3c..0e8b8b3d05 100644 --- a/test/Typecheck/Positive.hs +++ b/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")) diff --git a/tests/positive/ConstructorWildcard.juvix b/tests/positive/ConstructorWildcard.juvix new file mode 100644 index 0000000000..1698e294ea --- /dev/null +++ b/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;