The point AFAICT isn't that the type checker sees "bool -> bool" as an instance of "a -> a". Instead, the issue is that during type inference, when the compiler

The point AFAICT isn't that the type checker sees "bool -> bool" as an instance of "a -> a". Instead, the issue is that during type inference, when the compiler sees "m := not", it will infer that a == bool, i.e. that "m = ref (fn x ⇒ x)" was really "m = ref (fn (x:bool) ⇒ x)". But then it will forget that inference when type checking "print ((!m) 23)"; there it will infer that a == int, and that the original definition of m was really "m = ref (fn (x:int) ⇒ x)". Essentially the issue is that type inference forgets that it already solved for "a" and can't assign it to both "int" and "bool".