[Haskell-cafe] Type Family Relations

Cafe, I am wondering if there is a way to enforce compile time checking of an axiom relating two separate type families. Mandatory contrived example:

type family AddressOf h type family HeaderOf a

-- I'm looking for something to the effect of: type axiom HeaderOf (AddressOf x) ~ x

-- Valid: type instance AddressOf IPv4Header = IPv4 type instance HeaderOf IPv4 = IPv4Header

-- Invalid type instance AddressOf AppHeader = AppAddress type instance HeaderOf AppAddress = [AppHeader]

So this is a universally enforced type equivalence. The stipulation could be arbitrarily complex, checked at compile time, and must hold for all instances of either type family. Am I making this too hard? Is there already a solution I'm missing? Cheers, Tom