[Agda] Pattern-matching, unfortunate effect on type

[Andreas Abel]

Hi Florent,

could you please send the file or a self-contained snippet which  
reproduces the problem?

On Jan 28, 2010, at 6:53 PM, Florent Balestrieri wrote:
> 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)

My eyes are reading -4 here which has low probability of actually  
occurring there, so maybe something got screwed up by the emailer  
after all?

> 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

Cheers,
Andreas

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41