> A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments

LF does not have higher kinded types but it does have dependent types.