Me and Tom Schrijvers recently got a paper accepted at Haskell '17 concerning the elaboration of functional dependencies in System FC *without extending it*: https://people.cs.kuleuven.be/~george.karachalias/papers/fundeps.pdf https://people.cs.kuleuven.be/~george.karachalias/papers/fundeps.pdf The work is not currently implemented in GHC but we made some extra effort to make our system GHC-compatible so that integration will be possible in the future :-) In addition to the elaboration of FDs, we also noticed that they are unsound as currently implemented (Section 2.2 in the draft), if we treat them as type-level functions. Hence, we had to tighten up the restrictions imposed on them, good thing that until now they didn't affect the generated System FC code! There is still some work to be done to transfer the results to injective type families but I believe we are getting there :) Cheers, George -- View this message in context: http://haskell.1045720.n5.nabble.com/Trouble-with-injective-type-families-tp... Sent from the Haskell - Glasgow-haskell-users mailing list archive at Nabble.com.