I feel like there is worth expliciting that where in the signature you find the type variable or Never is important, and gives you different results.
You are right that html : String -> Html msg and html : String -> Html Never give you the same guarantee that the function will return any message. Specifically, this guarantee happens every time the Html is used with (lowercase) type variable that is only present once in the signature, and that the Html is the return value. If you find msg once more in the signature, like in html : msg -> Html msg you lose that guarantee.
Never comes in handy when you want the arguments of a function to be static (in the case of Html), so for instance html : Html Never -> Html msg. If you had done html : Html msg -> Html msg, you would not have that guarantee at all. I second the case @brian mentioned where the signature of tesk9/accessible-html's div function is List (Attribute Never) -> List (Html msg) -> Html msg. If it was List (Attribute msg) -> List (Html msg) -> Html msg, the guarantee that the div itself doesn’t trigger a message would be lost.