broken-scanl.idr

scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
scanl f q ls =  q :: (case ls of
                         []   => []
                         x::xs => scanl f (f q x) xs)

-- When elaborating left hand side of Main.case block in scanl:
-- When elaborating argument ls to Main.case block in scanl:
--         Can't unify
--                 Vect 0 a
--         with
--                 Vect n a
--         
--         Specifically:
--                 Can't unify
--                         0
--                 with
--                         n

bitsToFin : Bits n -> Fin (power 2 n)
bitsToFin = fromInteger . bitsToInt

causes

When elaborating right hand side of bitsToFin:
Can't resolve type class Num (Fin (power 2 n))