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

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.