Lack an explicit restriction on "return type" in the explicit function template instantiation/specialization

template<class T>
void fun(T){}

template<>
int fun(int){}

In the current draft, there's no formal provision that can prove the example is ill-formed. The only potential relevant rules are
[temp.deduct.decl] p2

If, for the set of function templates so considered, there is either no match or more than one match after partial ordering has been considered ([temp.func.order]), deduction fails and, in the declaration cases, the program is ill-formed.

"match" is vague and it is not sufficiently clear, consider the following example

template<class T>
auto fun(T){}

template<>
auto fun(int){
   return 0;
}

The above example is accepted by all implementations, what does "match" mean in this example?

@jensmaurer @opensdh

The "match" may have a clear definition instead. Such as

The function type of an explicit specialization shall be identical to the function type of the specialization that would be implicitly instantiated from the function template, except that, the function template has a declared return type that uses a placeholder type, which case is specified in [dcl.spec.auto].

The explicit instantiation declaration for a function template may have a similar restriction as to the above. Or, we should have a reference to [temp.deduct.decl] in a general rule for explicit specialization of a function template instead just mentions [temp.deduct.decl] in paragraph [temp.expl.spec] p10 that is not suitable for template<> void fun<int>(int);. BTW, since [temp.deduct.decl] p1 references to [temp.deduct.type] but that section lacks to specify the deduction of function type's return type with the form T.

Start by reading [temp.deduct.decl], [temp.expl.spec], and [dcl.spec.auto], then compare their rules with the two explicit-specialization examples in the issue. Determine how return-type matching and placeholder return types are specified for explicit instantiations and specializations. Done means the draft explicitly resolves whether both examples are well-formed and defines what “match” means.