Here's some sort specifications for LiquidHaskell (refinement types) https://github.com/ucsd-progsys/liquidhaskell/blob/master/te...

I have a bit of trouble reading it, but the specs are very terse.