Use notation N @⊆ E to avoid ambiguity.
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.