Hi,

I think that

...

...

...

class HeaderOf addr hdr | addr -> hdr does not enforce that there must be a corresponding instance AddressOf hdr addr. Hence, the type checker cannot use that information either. Do you have a way to remedy that?

I've often wanted something similar, and experimenting with this the following two options seem to be equivalent and work as desired: ----------------------------------------------------------------------------- -- both options share this code: -- | The crucial assertion ipv4 :: AddrHdrPair IPv4 IPv4Header ipv4 = AddrHdrPair data IPv4Header = C1 data IPv4 = C2 data AppAddress = C3 data AppHeader = C4 ----------------------------------------------------------------------------- -- OPTION(1): -- type families + GADT with equality constraints type family HeaderOf addr type family AddressOf hdr data AddrHdrPair hdr addr where AddrHdrPair :: (hdr ~ HeaderOf addr ,addr ~ AddressOf hdr) => AddrHdrPair addr hdr type instance HeaderOf IPv4 = IPv4Header type instance AddressOf IPv4Header = IPv4 ----------------------------------------------------------------------------- -- OPTION(2): -- classes + GADT with instance constraints class HeaderOf addr hdr | addr -> hdr class AddressOf hdr addr | addr -> hdr data AddrHdrPair hdr addr where AddrHdrPair :: (HeaderOf addr hdr ,AddressOf hdr addr) => AddrHdrPair addr hdr instance AddressOf IPv4Header IPv4 instance HeaderOf IPv4 IPv4Header ----------------------------------------------------------------------------- -- And commenting out the above instances in turn -- to verify that everything indeed works, and to -- compare error message content: {- -- type instance HeaderOf IPv4 = IPv4Header Cafe0.hs:9:0: Couldn't match expected type `HeaderOf IPv4' against inferred type `IPv4Header' When generalising the type(s) for `ipv4' Failed, modules loaded: none. -- type instance AddressOf IPv4Header = IPv4 Cafe0.hs:9:0: Couldn't match expected type `AddressOf IPv4Header' against inferred type `IPv4' When generalising the type(s) for `ipv4' Failed, modules loaded: none. -} {- -- instance AddressOf IPv4Header IPv4 Cafe0.hs:9:7: No instance for (AddressOf IPv4Header IPv4) arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17 Possible fix: add an instance declaration for (AddressOf IPv4Header IPv4) In the expression: AddrHdrPair In the definition of `ipv4': ipv4 = AddrHdrPair Failed, modules loaded: none. -- instance HeaderOf IPv4 IPv4Header Cafe0.hs:9:7: No instance for (HeaderOf IPv4 IPv4Header) arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17 Possible fix: add an instance declaration for (HeaderOf IPv4 IPv4Header) In the expression: AddrHdrPair In the definition of `ipv4': ipv4 = AddrHdrPair Failed, modules loaded: none. -} -- endcode ----------------------------------------------------------------------------- I'm not sure if there are any circumstances under which these two don't behave equivalently. All the best, Matt