If the reason you know your Maybe T is a Just _ is that you tested it locally: in any language that favors the Maybe pattern, the idiomatic way of performing that test makes the result available to the type system (destructuring / combinators / 'nads). On the other hand, if you know your Maybe is a Just because of non-local information, you will eventually turn out to be wrong :)
No, you can know -- and even prove -- that at a certain callsite, a Maybe would be a Just, and if you were using a dependent type system, you can prove that in the type system (although it probably won't be automatically inferred -- you may have to work hard for the proof), but Haskell's type system is too weak to express such properties and such proofs, at least in the general case.
