Dear Simon, You mentioned that GHC uses 'checking' when it knows the types. How this relates to 'unification', I don't know. It might very well be the same. Hopefully, the following example sheds a bit more light on what I mean (carefully nicked from Uktaad B'mal's "Beginning Faking It"). Examples are many, including in the "Understanding FDs via CHRs" paper. -- Start example To define 'vectors,' we need to code the length of a list in a type. With the zero/successor notation for naturals, we can do this is data constructors without term-level constructors: data Z data S x Vector concatenation requires addition of these numerals. In Prolog terms: Add(zero, X, X). Add(s X, Y, s Z) :- Add X Y Z We can translate this to a type class as class Add a b c | a b -> c instance Add Z x x instance Add x y z => Add (S x) y (S z) -- End example Because of your paper I understand why the coverage condition is in place and why it fails for the last of these instance declarations. GHC will allow me to do this by saying allow-undecidable-instances. As you state in the paper, the three FD-conditions of Coverage, Consistency and Bound Variable are sufficient, but not (always) necessary. I see why the example above causes considerable problems for inference, but if I read these instance declarations as Horn clauses, I see no problem at all in checking any actual occurrence in a program, i.e. if I write a concatenation function for vectors that uses this class as a property of vectors, I don't see where a type checker, using Prolog-like unification, runs into difficulties. What I'm probably asking (it's hard to tell, even for me, sometimes), is whether there is something between a type checker that is guaranteed to terminate and throwing all guarantees with regards to decidability right out the window. Again, I might be completely mistaken about how GHC does this. In that case I would like to find out where I make a wrongful assumption. Regards, Philip