(Hotmail is again swallowing newlines--sorry for the re-post) I see. The type inference algorithm requires type variables to be type constructors, not functions. Equality constraints are simplified assuming that is the case. I knew that type functions had to be fully applied, but I didn't know that they also couldn't be "taken apart" by unification. This explains why the following doesn't typecheck: type family T a :: * my_id :: f a -> f a; my_id = id x :: T a -> T a; x = my_id IMHO, this was not clear from the documentation or from the error message (It certainly _looks_ like "T a" should match "f a"...). Thanks for the explanation. -heatsink _________________________________________________________________ Hotmail: Trusted email with powerful SPAM protection. http://clk.atdmt.com/GBL/go/201469227/direct/01/