I have run into a similar problem to my last question which is not resolved with NoMonomorphismRestriction. 'foo2' has a partial type signature and I get an occurs check. 'foo3' is exactly the same except it has no signature, and it works! Why can't 'foo2' be inferred like 'foo3'? {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE NoMonomorphismRestriction #-} type family Quux a type family Corge a foo :: ( b ~ Quux a , a ~ Corge b ) => a -> b foo = undefined -- Occurs check: cannot construct the infinite type: -- t0 ~ Corge (Quux t0) -- arising from a use of ‘foo’ -- The type variable ‘t0’ is ambiguous -- foo2 :: _ foo2 = foo foo3 = foo