20070815-1

 module List (A : Set) where

  data List : Set where
    []   : List
    _::_ : A -> List -> List

 open List

 test : (A : Set) -> List A
 test A = [] A

Fixed.