Moving the dot patterns in this way could be confusing to the programmer. If an explicit dot pattern is moved, then it makes sense to emit a warning.

The dot patterns are not actually moved, instead Agda tries to reconstruct the LHS from scratch using iterated case splitting. If after this case splitting there is still some discrepancy, these are registered in the origin of the internal patterns by the code in https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rules/LHS.hs#L443-L462. One could conceivably emit a warning here if the patOrig p returns something other than PatODot in the case of a DotP.

If the dot pattern was not moved, then the code would presumably be accepted. Do we have to move it?

The dots are computed by the pattern unifier. It already has a system for priorities that it uses to decide which variable to instantiate: https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rules/LHS/Problem.hs#L113-L123. So it already prefers to instantiate variables that correspond to a dot pattern written by the user. I'll investigate further why that mechanism doesn't kick in in your test case.

Ah, I understand what's the problem now. When Agda does the case split on the constructor r, it has not yet performed the case split on the pair in the argument of d, so the argument of d is still just a variable. Since the unifier sees a variable being compared to a non-variable, the priorities are not taken into account and the variable is just solved. We could instead try to eta-expand the variable when comparing it to an expression of record type, but this could potentially cause unwanted eta-expansion (something that caused performance problems in the past).

I encountered this problem (but without any explicit dot patterns) in my code, and once I had understood its cause it was easy to fix it. However, the output of -vterm:20 is not very easy to read, and it is not easy to discover this option.

I think I am running into the same kind of problem, but with perhaps a simpler example, and I don't see any eta getting in the way here. Reporting partly in the hope that this will shed new light, and partly hoping to be told about a workaround.

{-# OPTIONS --cubical #-}

mutual
  data Ord : Set
  data _≤_ : Ord -> Ord -> Set

  data Ord where
    succ  : Ord -> Ord
    limit : (x y : Ord) -> (x<y : succ x ≤ y) → Ord

  data _≤_ where
    ≤-limiting  : ∀ x y x<y z -> (limit x y x<y) ≤ z

≤-ind : (P : {x y : Ord} → x ≤ y → Set) →
        (∀ x y x<y z → P x<y → P (≤-limiting x y x<y z)) →
        (x y : Ord) → (x≤y : x ≤ y) → P x≤y
≤-ind P l .(limit x y x<y) .z (≤-limiting x y x<y z) = l x y x<y z (≤-ind P l (succ x) y x<y)

This gives the error

Termination checking failed for the following functions:
  ≤-ind
Problematic calls:
  ≤-ind P l (succ x) y x<y

because the dot pattern has been "moved" from limit x y x<y to x<y in ≤-limiting, hence x<y is not seen as structurally smaller when dot patterns are not taken into account under --cubical.

It seems that the dots are moved because of forced constructor arguments. A workaround is to enable the flag --no-forcing. Perhaps this should be turned on by default for --cubical? (since we're currently not compiling cubical, turning off forcing doesn't actually hurt.)

Note that --no-forcing doesn't make a difference for the OP.

Perhaps this could be fixed by relaxing @Saizan 's fix of #4606 to still allow the termination checker to look into dot patterns if they are variables or record constructors.