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

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

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",

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
+	                  ^
+

tests/idris2/reg034/run

@@ -0,0 +1,3 @@
+$1 --check void.idr
+
+rm -rf build

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)