From 804d0da167dedf327fc5ff557c1b17038bd39661 Mon Sep 17 00:00:00 2001 From: Martin Fredin Date: Mon, 24 Apr 2023 10:10:15 +0200 Subject: [PATCH] Check number of arguments in pattern match --- src/ReportForall.hs | 2 -- src/TypeChecker/TypeCheckerBidir.hs | 5 ++++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ReportForall.hs b/src/ReportForall.hs index 8ac8515..8b5e9db 100644 --- a/src/ReportForall.hs +++ b/src/ReportForall.hs @@ -66,5 +66,3 @@ rpProgram rf (Program defs) = do ECase e bs -> rpuExp e >> mapM_ rpuBranch bs _ -> pure () -reportAnyForall :: Program -> Err () -reportAnyForall = undefined diff --git a/src/TypeChecker/TypeCheckerBidir.hs b/src/TypeChecker/TypeCheckerBidir.hs index b62e587..9c90531 100644 --- a/src/TypeChecker/TypeCheckerBidir.hs +++ b/src/TypeChecker/TypeCheckerBidir.hs @@ -396,10 +396,13 @@ checkPattern patt t_patt = case patt of -- Γ ⊢ K p₁ p₂ ↑ B ⊣ Δ PInj name ps -> do t_inj <- maybeToRightM "unknown constructor" =<< lookupInj name + let ps' = getParams t_inj + unless (length ps' == length ps) $ + throwError "Wrong number of arguments!" sub <- substituteTVarsOf t_inj subtype (sub $ getDataId t_inj) t_patt let checkP p t = checkPattern p =<< apply (sub t) - ps' <- zipWithM checkP ps $ getParams t_inj + ps' <- zipWithM checkP ps ps' apply (T.PInj (coerce name) (map fst ps'), t_patt) where substituteTVarsOf = \case