Do early occur-check in unification to allow eta to fire (fixes bug #3477)
Allow pattern matching on the applied form of projections with primitive
applications, solving part of bug #3503.
Fix unification which was failing when unifying a primitive projection against
its expansion if it could reduce (fixes bug #3480).