In the implementation for getPrefix in section 11.1.4 in step 4, you show the following hole:

  a : Type
  k : Nat
  value : a
  xs : Inf (InfList a)
--------------------------------------
getPrefix_rhs_1 : List a


… and finish the implementation with the clause

getPrefix (S k) (value :: xs) = value :: getPrefix k (Force xs)


However, this is not what I'm seeing in Idris 0.99. The Inf has already been removed and I don't need a Force:

- + Main.getPrefix_rhs_1 [P]
 `--                     a : Type
                         k : Nat
                     value : a
                        xs : InfList a
     ----------------------------------
      Main.getPrefix_rhs_1 : List a


The next section talks about how Idris will implicitly insert Delay and Force for you. Has any of this behaviour changed between 0.12 and 0.99?

Here's the complete code:

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z _ = []
getPrefix (S k) (value :: xs) = ?getPrefix_rhs_1
In section 11.1.4, we're implementing the function getPrefix : (count : Nat) -> InfList ty -> List ty.

A (very) minor nitpick: the type variable changes from ty to a when showing the implementation below. smilie
V13, section 8.6.2:

“By using Dec, you’ve been able to write explicitly in the type what checkEqNat is supposed to do: run either a proof that the inputs are equal, or a proof that they’re not.”


Should this be “return either a proof […]”?
Turns out that my own Vect definition was wrong… Sorry for the noise. smilie
(MEAP v12, Idris 0.12.3)

In exercise 8.2.6.2, if I type in the skeleton definition in the book:

my_reverse : Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


… I don't get the nice listing of holes, but instead the following error:


     When checking left hand side of Main.my_reverse, reverse':
     Type mismatch between
             Vect {a = Type} (S k) a (Type of x :: xs)
     and
             Vect {a = ty} (S k) a (Expected type)
     
     Specifically:
             Type mismatch between
                     Type
             and
                     ty


After some fumbling around, I found a way to make the error go away, but I don't really know why this works, nor what the original error meant.

my_reverse : {a : Type} -> Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : {a : Type} -> Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


Is this expected behaviour here? Did I do something wrong?
In V03 chapter 2 you write “This begs the question: when is it a good idea to use the qualified style (with the module name prefixed) over the unqualified style?”. While I know that “begging the question” colloquially means “raising the question” instead of its original meaning from logic, you'll save yourself two angry emails if you change it to “raises the question”. smilie
In the note ‘IO in Haskell and Idris’, in the setence ending with ‘you can safely move on to Section   “Reading and Validating Dependent Types”’, the link takes me to the start of chapter 5. I'm using the epub verision in iBooks.
I also see this error with version 0.9.20.
I'd also like to learn more about this.

A couple of things I can think of:

- Not possible(?) to do full type inference à la ML
- Need to define types and functions before use, so ordering is important and `mututal` blocks are needed when function a calls function b which calls function a again.