+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 depend

+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.