> So, is it that the functor is being checked at the point of definition, > as well as it's instantiation at functor application? Yes. Both are checked. > Does that mean that a functor argument isn't matched against it's > argument signature, it's just expanded and rechecked? A functor argument is matched against the functor argument signature and then the body is re-elaborated.