Example of type checker not being able to unify stuff after inlining a function

inline_fail.idr

data IsEmpty : List Char -> Type where
    Empty : IsEmpty []

Uninhabited (IsEmpty (x::xs)) where
    uninhabited Empty impossible

decideIsEmpty : (cs : List Char) -> Dec (IsEmpty cs)
decideIsEmpty cs = case cs of
    [] => Yes Empty
    (x :: xs) => No uninhabited

decideIsEmptyString : (s : String) -> Dec (IsEmpty (unpack s))
decideIsEmptyString s = decideIsEmpty (unpack s)

decideIsEmptyString' : (s : String) -> Dec (IsEmpty (unpack s))
decideIsEmptyString' s = case unpack s of
    [] => Yes Empty
    (x :: xs) => No uninhabited

decideIsEmptyString'' : (s : String) -> Dec (IsEmpty (unpack s))
decideIsEmptyString'' s = case unpack s of
    [] => Yes Empty
    (x :: xs) => No ?_