Hi Jonas Thanks - I was anticipating a type like this for the destructor: viewl :: Finite s a -> Either () (a, Finite (Predecessor s) a) I didn't appreciate that the size type in your code represented the upper bound and not the actual size. Best wishes Stephen