The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies` language extension. GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a series of papers 2005 to 2008, and IIRC the development wasn't finished in full in GHC until after that. (Superclass constraints took up to about 2010.) Suppose I wanted just the (~) parts of those implementations. Which would be the best place to look? (The Users Guide doesn't give a reference.) ICFP 2008 'Type Checking with Open Type Functions' shows uses of (~) in user-written code, but doesn't explain it or motivate it as a separate feature. My specific question is: long before (~), it was possible to write a TypeCast class, with bidirectional FunDeps to improve each type parameter from the other. But for the compiler to see the type improvement at term level, typically you also need a typeCast method and to explicitly wrap a term in it. If you just wrote a term of type `a` in a place where `b` was wanted, the compiler would either fail to see your `TypeCast a b`, or unify the two too eagerly, then infer an overall type that wasn't general enough. (For that reason, the instance for TypeCast goes through some devious/indirect other classes/instances or exploits separate compilation, to hide what's going on from the compiler's enthusiasm.) But (~) does some sort of magic: it's a kinda typeclass but without a method. How does it mesh with type improvement in the goldilocks zone: neither too eager nor too lazy? AntC