[Agda] list member error

[Andreas Abel]

On 28.12.12 7:47 PM, Serge D. Mechveliani wrote:
> data Elem {c l : Level} {A : Setoid c l} :
>         Setoid.Carrier A -> List (Setoid.Carrier A) -> Set (suc (max c l))
>
>    -- "x  is in the list  xs  by _~~_"
>    where
>    inHead : let open Setoid {{...}} in
>                      (x y : Carrier) -> x ~~ y -> (xs : List Carrier) ->
>                                                            Elem x (y :: xs)
>    inTail : let C = Setoid.Carrier A
>             in  (x y : C) -> (xs : List C) -> Elem x xs -> Elem x (y :: xs)

Agda cannot guess parameter {A} of the recursive call to Elem.  It works 
if you add {A = A}.

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
module ListMem where
open import Foreign.Haskell
open import IO.Primitive
open import Data.String as String using (toCostring)
open import Level           using (Level; suc; _?_)
open import Relation.Binary using (Setoid; module Setoid)
open import Data.List       using (List; []; _?_)

data Elem {c l : Level} {A : Setoid c l} :
       Setoid.Carrier A -> List (Setoid.Carrier A) -> Set (suc (_?_ c l))

  -- "x  is in the list  xs  by _~~_"
  where
  inHead : let open Setoid {{...}} in
                    (x y : Carrier) -> x ? y -> (xs : List Carrier) ->
                                                          Elem x (y ? xs)
  inTail : let C = Setoid.Carrier A
           in  (x y : C) -> (xs : List C) -> Elem {A = A} x xs -> Elem x (y ? xs)

main : IO Unit
main = putStrLn (toCostring "done")