> If you view functors as being checked once, then the fact that there > exists, for each arm of the case, a structure you could apply the > functor to which would result in that arm being the one followed is > enough. Exactly. Defunctorization and redundancy checking of the match for each functor application is the reason why MLton reports the warning and the other SML compilers don't.