+1. If the language is not pure it's unclear how type checking would work. To make things even clearer, consider the following example (in a hypothetical dependently typed language with mutable references):

   f : () -> Type
   f =
     let r = ref 0 in
     fun () ->
       let t = if !r = 0 then Int else String in
       r := r + 1;
       r

   x : f ()
   x = 17

   y : f ()
   y = "foo"

Should this program type check? I think there is a consistent way to talk about type checking here (if there is a canonical ordering of all definitions across all files) but it seems unlikely you'll get a system that's easy to understand.