checkParameters
  d                   = Test201.X.Foo
  d0 (should be == d) = Test201._._.Foo
  dc                  = Test201._._.Foo
  vs                  = []
  pars                = [Set]

hm.

The is that the copy of Foo in the parametrised module has a clause with arguments,

  dataClause     =
    (a : Set) |- (a = a@0) = Test201.X.Foo (Set -> Set) : Set

but checkParameters is trying to reduce it with no arguments, so appDefE' thinks it's fine to skip that clause. I suppose the fix would be to change checkParameters to pass the module telescope we should be under, but the module telescope can get refined by pattern matching, and I have no idea how to go about reconstructing it. (@jespercockx?)

(I'm not sure how known this is, but it's a bit surprising to me that during LHS checking, the checkpoints are completely incorrect: if I complicate the reproducer slightly, and add a bunch of prints, Agda seems to be telling me that the way to substitute a term from context-telescope (b : Set) (A : Nat) (B : Nat) to (a : Wrap) (b : Set) is to weaken it by 3:

  gamma  = (b : Set) (A : Nat) (B : Nat)
  mod    = Test201._
  delta  = (a : Wrap) (b : Set)
  sub    = wkS 3 idS
  ourmod = 42
  ckp    =
    {0 -> wkS 5 idS, 41 -> wkS 4 idS, 42 -> wkS 3 idS,
     169 -> wkS 2 idS, 170 -> wkS 1 idS, 171 -> idS}

Edit -- I suppose I've run into the LHS checker having weird checkpoints in the past.)

The is that the copy of Foo in the parametrised module has a clause with arguments,

  dataClause     =
    (a : Set) |- (a = a@0) = Test201.X.Foo (Set -> Set) : Set

but checkParameters is trying to reduce it with no arguments, so appDefE' thinks it's fine to skip that clause. I suppose the fix would be to change checkParameters to pass the module telescope we should be under, but the module telescope can get refined by pattern matching, and I have no idea how to go about reconstructing it. (@jespercockx?)

That's what getModuleParameterSub and its ilk are for, unless I'm missing something?

Regarding checkpoints in the LHS checker, they are indeed not correct at the moment since the LHS checker does not actually make use of checkpoints! It just computes telescopes and substitutions the manual way. Only once we go to the RHS we actually perform the modifications to the context (and thus insert the new checkpoint). The reason is simply that the LHS checker predates the checkpoint machinery, and no-one went through the trouble of rewriting it the proper way using checkpoints.

The feature is crucial for programmers. For example, a program must not confuse of what is happening in the domain of the module OfVector(n) and in the domain of the module OfVector(suc n). In particular, I use inductive proofs on such parameter n.
I am not sure, I have a slight suspicion that this bug was also in earlier Agda versions.

For any occasion, I copy here my bug report from Zulip.

This is on Agda version 2.7.0.1
Built with flags (cabal -f) - optimise-heavily: extra optimisations, ghc-9.0.2, stdlib-2.1.1

Type checking:

agda $agdaLibOpt --auto-inline --guardedness Test.agda

Below test needs an argument of type Vector'
while it is given the pattern (vec _ _) which has a different type.

And Agda does not report of the error.

module Test where
open import Data.List using (List; length)
open import Data.Nat using (ℕ; suc)
open import Relation.Binary.PropositionalEquality using (_≡_)

module OfVector {α} (A : Set α) (n : ℕ)
  where
  data Vector : Set α  where
                       vec : (xs : List A) → length xs ≡ n → Vector

module Test (m : ℕ)
  where
  open OfVector ℕ m       using (Vector; vec)         -- vectors of length m
  open OfVector ℕ (suc m) using ()                    -- vectors of length 1+m
                          renaming (Vector to Vector'; vec to vec')
  test : Vector' → ℕ
  test (vec _ _) = 0

If m and (suc m) are changed to 1 and 2 respectively, then the error is reported.

That's what getModuleParameterSub and its ilk are for, unless I'm missing something?

Well, unfortunately

getModuleParameterSub :: (MonadTCEnv m, ReadTCState m) => ModuleName -> m (Maybe Substitution)
getModuleParameterSub m = do
  mcp <- (^. stModuleCheckpoints . key m) <$> getTCState
  traverse checkpointSubstitution mcp

So it's not helpful here. I couldn't figure out how to compute the substitution to the module context in the middle of pattern matching since AFAICT splitCon doesn't have immediate access to the previous LHSState (and so the previous patterns), though it might be sufficient to disambiguateConstructor in updateProblemEqs, in which case it might not be too hard to compute.