Two examples from the top of my head:
1. Encoding matrix sizes into the data- and function-types, so that you can safely have a function `mat[c,b] mat_mult(mat[a,b] a, mat[c,d] b)` or even `mat[w-2,h-2] convolve(mat[w,h] input, mat[3,3] kernel)` and have the compiler check that you never use a matrix of the wrong size.
2. Actually checking the correctness of your implementation.
There is a very nice online demo of Liquid Haskell [1], where they defined the properties of ordered lists (each element has to be smaller or equal to the one before, line 119). Then they define a function that takes an (unordered) list and spits out a ordered one by applying a simple quicksort.
Now, if you break the algorithm (e.g. flip the < in line 193) and run Check, the compiler will tell you that you messed up your sorting algorithm.
Pretty neat.
edit: I just realized that LiquidHaskell is almost 10 years old. Sad to see that basically nothing made it into "production".
