[Agda] simple with->case fail

[Andreas Abel]

Please always post self-contained examples!

On 25.08.2015 21:48, mechvel at scico.botik.ru wrote:
> People,
> I have
>
>   f :  ∀ x → ¬ AnyRepeats (gfilter toSubsetIf (x ∷ []))
>   f x  with member? x
>   ...  | yes _ = noRepetition[x]
>   ...  | no _  = noRepetition[]
>
> which is type checked in  Agda 2.4.2.3.
> But its `case' version
>
>   f x = case member? x of \ { (yes _) → noRepetition[x]
>                             ; (no _)  → noRepetition[] }
>
> leads to the report
>
>    _x_170 x ∷ [] != [] of type List subC
>    when checking that the expression noRepetition[] has type
>    (AnyRepeats (_x_170 x ∷ []) → ⊥)
>
> Is the first version  noRepetition[]  has the needed type,
> and in the second has not.
>
> May this be all right for the type checker?
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/