Idris can't disambiguate between Vect.:: and List.::

[Ashwin Bhaskar]

This is my program

transposeMat1 : Vect n (Vect m a) -> Vect m (Vect n a)
transposeMat1 [] = createEmpties
transposeMat1 (x :: xs) = let xsTransposed = transposeMat1 xs
                              xMapped = map (\x => x Data.Vect.:: Nil) x in
                              zipWith (Data.Vect.::) xMapped xsTransposed

I get the type error

When checking right hand side of transposeMat1 with expected type Vect m (Vect (S len) a) When checking argument func to function Prelude.Functor.map: Can't disambiguate since no name has a suitable type: Prelude.List.::, Prelude.Stream.::, Data.Vect.::

What am I doing wrong here?

[alru...@gmail.com]

Your syntax for qualifying operator names is a bit off. In order to refer to Vect's cons, (Data.Vect.::) won't work, but Data.Vect.(::) will. I also really enjoy that you can omit the Data. from this, leaving just Vect.(::).

When qualifying an operator's name, we also can't use it infix, so rather than x Vect.(::) Nil we need Vect.(::) x Nil.

Beyond that, the type-checker will probably help get you back on track.

Error: While processing right hand side of transposeMat1. When unifying Vect m (Vect len a) and Vect m (Vect ?len (Vect 1 a)).
Mismatch between: a and Vect 1 a.

ListDisambiguate.idr:6:62--6:74
 2 | transposeMat1 : Vect n (Vect m a) -> Vect m (Vect n a)
 3 | transposeMat1 [] = ?createEmpties
 4 | transposeMat1 (x :: xs) = let xsTransposed = transposeMat1 xs
 5 |                               xMapped = map (\x => Data.Vect.(::) x Nil) x in
 6 |                               zipWith Data.Vect.(::) xMapped xsTransposed
                                                                  ^^^^^^^^^^^^

Cheers,

Alex