> The body of a functor is elaborated when the functor is defined. If > -warn-match is true, then the body is re-elaborated at each > application of the functor. Is that just to catch the cases when there are exceptions (used in patterns) in the argument of the functor? Still, it's rather confusing to have the error message refer to the functor body, not the functor application.