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 ++ "."

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

  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

These are just two functions that wrap and unwrap a string. Your "type" doesn't generate a compile-time error when constructed with the wrong data. This doesn't even handle the simplest use case:

   putStrLn (toString (fromString "something."))

Not to mention that to be truly useful a static type would need some sort of literal that would emit a compile-time error if the supplied init data was wrong.

In short, examples above do not demonstrate Haskell's ability to statically enforce rules like "string needs to end with a dot".

Now, you could make a type that always prepends a dot when asked for a string representation, which happens to enforce this specific constraint, but you cannot use a trick like this for most constraints (such as the second example of "only alpha characters").

That’s not true, you can wrap these in types that can only be constructed from valid data, and from that point on you can be sure everything is correct.

  data EndsWith : Type where
    EndsWithPeriod : (s: String) -> { auto prf : ("." `Strings.isSuffixOf` s = True) } -> EndsWith

  s : EndsWith
  s = EndsWithPeriod "."

  -- Value of type False = True cannot be found
  -- s2 : EndsWith
  -- s2 = EndsWithPeriod ""

Am I to presume you do all your programming in assembly (or opcodes?), since you never need to distiguish integers from strings in your source code?

> Gödels incompleteness theorems

is never relevant in the real world.

In the general case, all real computers are broken.