Since nclose : namespace → coPset is declared as a coercion, the notation nclose N ⊆ E was pretty printed as N ⊆ E. However, N ⊆ E could not be typechecked because type checking goes from left to right, and as such would look for an instance SubsetEq namespace, which causes the right hand side to be ill-typed.