steshaw (13) [Avatar] Offline
The definition of ListLast in the book is incorrect:
data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (init : List a) -> (x : a) -> ListLast (xs ++ [x])

This was a bit difficult to spot since it compiles OK. For the NonEmpty constructor, the result type should read ListLast (init ++ [x]).

As a side-node, I've noticed this kind of thing happening from time to time with Idris (i.e. typos/mistakes introducing an implicit variable that isn't "connected" to the rest of the definition). I wonder if it might be possible for Idris to detect these situations?
steshaw (13) [Avatar] Offline
A little followup. When starting to define describe_help, it's probably better to start with List Int, rather than the given List a:
describe_help : (input : List a) -> (form : ListLast input) -> String
describe_help input form = ?describe_help_rsh

Otherwise it's easy to get into a situation such as:
describeHelp : (input : List a) -> (form : ListLast input) -> String
describeHelp [] Empty = "Empty"
describeHelp (init ++ [x]) (NonEmpty init x) = "Non-empty, initial portion =   " ++ show init

This code fails to compile with an unhelpful message:
When checking right hand side of describeHelp with expected type

Can't disambiguate since no name has a suitable type:
Prelude.List.++, Prelude.Strings.++

This happens because of the code: ++ show init. Unfortunately, there is no implementation of Show for a (the element type of the list).

Note that the refine step in the book does switch the type to List Int but it's easy to miss as I did.
Edwin Brady (65) [Avatar] Offline
I think I did mean it to be List Int all along too... I think I've edited the final definition here but missed the earlier ones. Thanks for spotting.

That's a good idea about the implicit error message too - it's a mistake I sometimes make. I'll have to think about the implications (it will sometimes be intentional after all) but some kind of warning does seem useful.
steshaw (13) [Avatar] Offline
I was hoping that it would be possible to have an error message but I spotted another example later in the book which has an implicit introduced in the result type (Ex and they probably come up more often than I was thinking. Pity because I've really been struggling sometimes to find the source of the error. Still, you've always got a compiling version in the source code for the book but I find I learn more if I can avoid using that except when necessary.
Edwin Brady (65) [Avatar] Offline
Even in this case, you could suppresss the warning with an implicit binding `{rest : _} ->` so maybe it's not so bad. But there's also situations which will come up later (in Chapter 13/14) involving state machines in types where this would start to get a bit noisy.

I'll try to think of something anyway...