[Agda] list member error

[Serge D. Mechveliani]

Please, what is wrong in the below program?

(Agda-2.3.2, MAlonzo, lib-0.6, Debian Linux,

in the below source I replace  \sqcup --> max,  \:: --> ::,  \~~ --> ~~
)

---------------------------------------------------------------------
module Main where
open import Foreign.Haskell
open import IO.Primitive
open import Data.String as String using (toCostring)
open import Level           using (Level; suc; max) 
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 (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)

main : IO Unit
main = putStrLn (toCostring "done") 
---------------------------------------------------------------------
       
For example, I intend the following proof for  Elem 1 [3, 1] :

  let p : Elem 1 [1]
      p = inHead 1 1 1~~1 []
  in
  inTail 1 3 [1] p 

(is the above definition all right?)

The report concerns the two lines for  inTail :

------------------------------------------------------------------------
Finished Main.

Unsolved metas at the following locations:
  /home/mechvel/doconA/0.01/reports/2/Main.agda:17,12-18,74
  /home/mechvel/doconA/0.01/reports/2/Main.agda:18,46-50
------------------------------------------------------------------------

Does  "Finished Main"  mean that the error occurs after the type checking?

The precise code is attached here as  Main.agda.zip. 

Thanks,

------
Sergei
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 553 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20121228/050b9d8c/Main.agda.zip