[Agda] Pattern-matching, unfortunate effect on type

[Florent Balestrieri]

Hello,

I just can't figure this out. I always believed that the type
of an argument would be the same before and after refining
its pattern. Obviously, it might have an impact on the type
of other arguments, but not its own, right?

However this interaction session shows the opposite:
I hope the utf is not wrecked by my email agent.

Before refining a pattern consisting of a variable u with type:

    | u   : x ∷ xs ≈ h ∷ .Data.Colist.♯-4 h ♯t (x ∷ xs)

it seems reasonable to pattern match on it, replacing `u' by

    | .h ∷ xs≈

but then I get the following message:

    | x ∷ ys' != w ++ x ∷ xs of type Colist A
    | when checking that the pattern .h ∷ xs≈ has type
    | x ∷ xs ≈ w ++ x ∷ xs

So after case-splitting agda does not give the same goal type
for the same argument, as if some dependency was lost in the
process.

All the best,
-- Florent