Fixity and associativity control at least at the haskell level. Notation comparable to Coq level. Generics without jvm limitations. Subtyping or subsets of inductive types. Rich signature overloading. No need for general recursion, loops etc. Pretty printing out of the box. Static literals (from the binary directly to memory).