Add reference to Stephen Dolan subtyping phd for infering pragma safe. It seems relevant but I have not read it fully yet.

propsals-ideas/Safe-functions-Calls.md

@@ -557,7 +557,9 @@ int foo(int b) | isprime(b) {return b;}
 Here the prechecks performed on `a` contain all the checks that foo performs on b. 
 As long as `a` is not reassigned here then we know that the predicates `a>2` and `isprime` hold for `a`at the call to foo. Thus, foo could be inferred as safe. 
 
-This requires binding the predicate expressions to the variable assignments. 
+> Read https://www.cs.tufts.edu/comp/150FP/archive/stephen-dolan/thesis.pdf ?
+
+This might require binding the predicate expressions to the variable assignments. 
 If the compiler supports this it should be able to infer `#pragma safe`.
 With the example above, the compiler could look up the checks that foo does on its input and then look up the set of predicates of the argument given. For instance a function called `pred` that takes a function name and the name of an input and returns the set of predicates which hold for that input variable. I think it's a good idea to replace the binding of input variable itself with a Greek letter so that you can easily compare sets of predicates. I chose $I$ iota for this to refer to identity.