I was trying to re-implement the Vect data type to become more familiar with the dependent types. This is what I wrote:
data Vect : (len : Nat) -> (elem : Type) -> Type where
Nil : Vect Z elem
(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] y = y
append (x :: xs) y = x :: append xs y
I can define, for example Vect 4 Nat and others as well. But if I try append (Vect 4 Nat) (Vect 3 Nat) I get an error that I am not able to parse:
When checking an application of function Main.append:
Type mismatch between
Type (Type of Vect len elem)
and
Vect n elem (Expected type)
Clearly there is something wrong in the way I think about this.
Any suggestion?
Also when I try to create Vect 4 [1,2,3,4] I get an error:
When checking argument elem to type constructor Main.Vect:
Can't disambiguate since no name has a suitable type:
Prelude.List.::, Main.::, Prelude.Stream.::
So I guess I am quite lost ...
Your definition of Vect and append look fine to me, but it's how you're creating values that's the problem. You're mixing up the type constructor Vect with the data constructors Nil and ::. You should create values of type Vect len elem with calls to Nil and ::.
In particular, Vect 4 Nat is a type, but append expects a value of that type, like 1 :: 2 :: 3 :: 4 :: Nil (or [1,2,3,4] which is just syntactic sugar for the former).
And Vect 4 [1,2,3,4] isn't possible since [1,2,3,4] is a value not a Type