Example from Idris TDD book does not work

[roehst]

Please attach complete source files that exhibit the issue in addition
to quoting from them here.

Steps to Reproduce

I am at the matrix transpose exercise. (page 77)

module Main

import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties = ?createEmpties_rhs1

transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose [] = createEmpties
transpose (x :: xs) = let xsTrans = transpose xs in ?the_rest

Expected Behavior

The code should type check and I should be able to extract ?the_rest as a lemma and continue the exercise.

Observed Behavior

Idris can not infer type.

     When checking right hand side of Main.transpose with expected type
             Vect n (Vect (S len) elem)
     
     Can't infer type for {letval_612}

My idris version is 1.3.1

[workflow]

Hi @roehst, it looks like this is some weird naming clash with the identifier transpose.

Try renaming transpose to something else, this code worked for me:

import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties = ?createEmpties_rhs1

transposeMatrix : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMatrix [] = createEmpties
transposeMatrix (x :: xs) = let xsTrans = transposeMatrix xs in
                          ?the_rest

[workflow]

The error message should definitely improve here!