Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items

val one : a ::: Type -> a -> a
val two : a ::: Type -> b ::: Type -> a -> b