In Idris, how to add 1 to a Fin until a "max" is Reached

Question

I have a data type which takes a number in constructor, and this number MUST be between 1 and 5 (represented as 0..4):

import Data.Fin
data Stars = MkStars (Fin 5)

I want to create a function that add one to an existing star, and if it's already a 5 stars, doesn't do anything

I tried

addOneStar: Stars -> Stars
addOneStar (MkStars FZ) = MkStars (FS FZ)
addOneStar (MkStars (FS x)) = if x < 3 
                              then MkStars (FS (FS x)) 
                              else MkStars (FS x)

But it doesn't compile with the error :

Type mismatch between
            Fin 4 (Type of x)
    and
            Fin 3 (Expected type)

    Specifically:
            Type mismatch between
                    1
            and
                    0

Can someone explain to me why is there this error ? And How to fix it ?

Answer 1

Cactus' answer explains the problem and gives one possible solution. Since we have dependent types in Idris, though, I would at least advertise the possibility of a solution that makes use of that and could thus be seen as more idiomatic:

nextFin : (m : Fin (S n)) -> {auto p : (toNat m) `LT` n} -> Fin (S n)
nextFin {n = Z} FZ {p} = absurd $ succNotLTEzero p
nextFin {n = Z} (FS FZ) impossible
nextFin {n = S k} FZ = FS FZ
nextFin {n = S k} (FS l) {p} = let p = fromLteSucc p in
  FS $ nextFin l

This function takes as argument a proof that the given Fin is not the last one. This way you can be sure on the level of the type checker that the program never even tries to give you a nextFin for that.

If you don't want that, but rather something akin to the cited answer, you can also use strengthen together with with rules to avoid most of the cases:

nextFin : Fin (S n) -> Maybe $ Fin (S n)
nextFin m with (strengthen m)
  | Left k = Nothing
  | Right k = Just $ FS k