> Still no static types for "Strings that end with a dot" or "Strings that match [a-z]+"

Sure there are. :) Technically speaking, anyway. Here’s a type for “strings that end with a dot”:

  -- | A string that ends in the character '.',
  -- represented as a string without its trailing dot.
  newtype StringEndingInDot = StringEndingInDot String

  fromString :: String -> Maybe StringEndingInDot
  fromString str = case reverse str of
    '.':cs -> Just $ StringEndingInDot (reverse cs)
    _      -> Nothing

  toString :: StringEndingInDot -> String
  toString (StringEndingInDot str) = str ++ "."

And here’s a type for “strings that match [a-z]+”:

  data Letter = A | B | C | D | ... | X | Y | Z
  type StringAZ = NonEmpty Letter

Now, admittedly, I would never use either of these types in real code, which is probably your actual point. :) But that’s a situation where there is a pragmatic “escape hatch” of sorts, since you can create an abstract datatype to represent these sorts of things in the type system without having to genuinely prove them:

  module StringEndingInDot(StringEndingInDot, fromString, toString) where
    newtype StringEndingInDot = StringEndingInDot { toString :: String }

    fromString :: String -> Maybe StringEndingInDot
    fromString str = case reverse str of
      '.':_ -> Just $ StringEndingInDot str
      _     -> Nothing

You may rightly complain that’s a lot of boilerplate just to represent this one property, and it doesn’t compose. That’s where the “Ghosts of Departed Proofs” paper (https://kataskeue.com/gdp.pdf) cited in the conclusion can come in. It provides a technique like the above that’s a little more advanced, but brings back composition.