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)