@Lucas_Payr proposed adding refinement types a while back Elm-Refine: Proposal. I’m guessing nothing came of it but the idea would be that, for example, modBy’s type signature would be changed from
modBy: Int -> Int -> Int to modBy: IntWithoutZero -> Int -> Int and IntWithoutZero would be defined with a special syntax (there’s more discussion in the thread about what that could look like)
{-| @refine \int -> int /= 0
-}
type alias IntWithoutZero =
Int
The compiler would then verify that this condition holds everywhere modBy is called. I guess in cases where it can’t be proven, the user would need to write if value == 0 then ... else modBy value n or something.