Consider the following code:

    template<typename T>
    concept ctrue = true;
    template<typename U>
    concept refable = ctrue<U&>;

[temp.constr.normal] says the normal form of `refable<U>` is:

 * The normal form of `ctrue<U&>`
 * Which is the normal form of `true` with substituting `T&` for `U`
in the parameter mappings for each atomic constraint

What is the normal form of `true`? It is "an atomic constraint whose
expression is [`true`] and whose parameter mapping is the identity
mapping"

The term "identity mapping" is never used again, but it appears that
for the constraint `true` it is an empty mapping (as written in
non-normative Example 1 directly after). (This term should be
explicitly defined somewhere)

This leads to the normal form of `refable<U>` to be the atomic
constraint `true` with an empty parameter mapping, which means that
`refable<void>` is satisfied (because satisfaction just checks if the
parameter mapping can be substituted).

This is undesirable (as it seems like the concept tries to form
`void&` but it is still satisfied).

When trying to remedy this, we have to ask if we want these two
concepts to be able to subsume each other:

    template<typename T>
    concept a = ctrue<int>;
    template<typename T>
    concept b = ctrue<long>;

Currently, they technically normalise to the same atomic constraint,
but this may or may not be desired.

This could be fixed by including these types in the parameter mapping
regardless: Defining "identity mapping" as "the parameter mapping of
the names of every template argument to their values", and tweaking
[temp.constr.atomic]p2 so that it only uses template parameters that
appear in the expression (if we want the concepts `a` and `b` to
subsume each other)

Changing how constraint satisfaction is checked would work: Instead of
defining it in terms of the normal form ([temp.names]p8 or
[temp.constr.decl]p3; [temp.names]p9), define it in terms of the
concept-ids themselves (+ other types of constraints introduced by
`requires`). There would be 4 types of concepts, conjunctions,
disjunctions, atomic constraints and concept-ids, the first 3 of which
already exist. A concept-id is satisfied exactly like an atomic
constraint: If its parameters can be substituted without resulting in
an invalid type or expression and it evaluates to `true`.

A different approach is to create a new type of associated constraint
that has all the substitutions made during normalization and may or
may not be checked for the purpose of subsumption, and only checks if
a valid type/expression/class template is formed.

The first approach seems to work fine, but I'm not sure if there are
some edge cases I haven't thought about. The second approach is closer
to what existing implementations (clang, msvc) already do*. The last
one is the easiest to reason about. *gcc seems to follow the standard
strictly (normalising first, discarding types not used in atomic
constraints): https://godbolt.org/z/P73bxrvr4

And as a side note, the last sentence of [temp.constr.normal]p(1.4)
("If any such substitution results in an invalid type or expression,
the program is ill-formed; no diagnostic is required.") should
probably be [temp.res.general]p6, with all the other ill-formed NDR
cases with templates.


Obviously the alternative way of writing `refable` with a requires
expression is preferable, but there are other more subtle cases where
this is unintuitive, and the question of constraint
equivalence/subsumption when at least one of their template parameters
is not used in any atomic constraint still stands. I believe this to
be a defect of the current standard, but I could write it up as a new
proposal. The backwards compatibility doesn't seem like an issue since
existing implementations don't agree on how to implement this (and the
"identity mapping" ambiguity).

If this was actually intended, I guess the behaviours of clang and
msvc would need to be fixed, and perhaps compilers would need to add a
warning about a concept which doesn't use all of its template
parameters.