From 04e05e3f863c20f5b8b4039caff22fcc5167df98 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 10 Aug 2020 14:03:34 +0100 Subject: [PATCH] Fix repeated argument check As it was, it could break if the argument was repeated more than twice. When checking dot patterns, we need to check that no further holes are solved, and that the pattern variable doesn't unify with some other pattern variable, but if it had already made progress (either for a good or bad reason) we missed this. Fixes #536 --- src/Core/Unify.idr | 31 ++++++++++++++++++++----------- tests/Main.idr | 2 +- tests/idris2/reg034/expected | 6 ++++++ tests/idris2/reg034/run | 3 +++ tests/idris2/reg034/void.idr | 21 +++++++++++++++++++++ 5 files changed, 51 insertions(+), 12 deletions(-) create mode 100644 tests/idris2/reg034/expected create mode 100755 tests/idris2/reg034/run create mode 100644 tests/idris2/reg034/void.idr diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index abe3f2460..5467698ae 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -1586,6 +1586,13 @@ checkDots ust <- get UST put UST (record { dotConstraints = [] } ust) where + getHoleName : Term [] -> Core (Maybe Name) + getHoleName tm + = do defs <- get Ctxt + NApp _ (NMeta n' i args) _ <- nf defs [] tm + | _ => pure Nothing + pure (Just n') + checkConstraint : (Name, DotReason, Constraint) -> Core () checkConstraint (n, reason, MkConstraint fc wl blocked env x y) = do logTermNF 10 "Dot" env y @@ -1595,8 +1602,10 @@ checkDots ust <- get UST handleUnify (do defs <- get Ctxt - Just olddef <- lookupDefExact n (gamma defs) - | Nothing => throw (UndefinedName fc n) + -- get the hole name that 'n' is currently resolved to, + -- if indeed it is still a hole + (i, _) <- getPosition n (gamma defs) + oldholen <- getHoleName (Meta fc n i []) -- Check that what was given (x) matches what was -- solved by unification (y). @@ -1605,25 +1614,25 @@ checkDots -- must be complete. cs <- unify inMatch fc env x y defs <- get Ctxt - Just ndef <- lookupDefExact n (gamma defs) - | Nothing => throw (UndefinedName fc n) -- If the name standing for the dot wasn't solved -- earlier, but is now (even with another metavariable) -- this is bad (it most likely means there's a non-linear -- variable) - let hBefore = case olddef of - Hole _ _ => True -- dot not solved - _ => False - let h = case ndef of - Hole _ _ => True -- dot not solved - _ => False + dotSolved <- + maybe (pure False) + (\n => do Just ndef <- lookupDefExact n (gamma defs) + | Nothing => throw (UndefinedName fc n) + case ndef of + Hole _ _ => pure False + _ => pure True) + oldholen -- If any of the things we solved have the same definition, -- we've sneaked a non-linear pattern variable in argsSame <- checkArgsSame (namesSolved cs) when (not (isNil (constraints cs)) - || (hBefore && not h) || argsSame) $ + || dotSolved || argsSame) $ throw (InternalError "Dot pattern match fail")) (\err => case err of diff --git a/tests/Main.idr b/tests/Main.idr index bde5db19f..ae08592d4 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -104,7 +104,7 @@ idrisTests "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014", "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021", "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", - "reg029", "reg030", "reg031", "reg032", "reg033", + "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", -- Totality checking "total001", "total002", "total003", "total004", "total005", "total006", "total007", "total008", "total009", diff --git a/tests/idris2/reg034/expected b/tests/idris2/reg034/expected new file mode 100644 index 000000000..59a929236 --- /dev/null +++ b/tests/idris2/reg034/expected @@ -0,0 +1,6 @@ +1/1: Building void (void.idr) +void.idr:18:19--18:20:While processing left hand side of Calc at void.idr:18:1--20:1: +Can't match on ?y [no locals in scope] (Non linear pattern variable) at +18 Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der + ^ + diff --git a/tests/idris2/reg034/run b/tests/idris2/reg034/run new file mode 100755 index 000000000..9c53c9299 --- /dev/null +++ b/tests/idris2/reg034/run @@ -0,0 +1,3 @@ +$1 --check void.idr + +rm -rf build diff --git a/tests/idris2/reg034/void.idr b/tests/idris2/reg034/void.idr new file mode 100644 index 000000000..11ee407d3 --- /dev/null +++ b/tests/idris2/reg034/void.idr @@ -0,0 +1,21 @@ +infixl 0 ~~ +prefix 1 |~ +infix 1 ... + +public export +(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z) +(...) x pf = (x ** pf) + +public export +data FastDerivation : (x : a) -> (y : b) -> Type where + (|~) : (x : a) -> FastDerivation x x + (~~) : FastDerivation x y -> + (step : (z : c ** y ~=~ z)) -> FastDerivation x z + +public export +Calc : {x : a} -> {y : b} -> FastDerivation x y -> x = y +Calc (|~ x) = Refl +Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der + +bad : Z = S Z +bad = Calc $ |~ Z ~~ Z ...(Refl)