[cfe-commits] Modulo renaming [WAS: r60615 ...]

[Gabor Greif]

Eli wrote:
> > Doug wrote:
> > With dependently-sized array types, we need them
> > to be unique so that we can determine that the types of the arrays
> > match in the parameter types of the functions "f" below:
> >
> >        template<int I, int J> void f(int (&array)[I+J]);
> >        template<int X, int Y> void f(int (&array)[X+Y]) { ... }
> >
> > If we don't realize that those canonical types match, we'll think  
> that
> > the definition is actually an overload rather than a redeclaration.
> > Not good!
>
> Ouch, seems like a pain to implement.
>
> -Eli

The metaprogramming community has solved this problem already,
http://www.cl.cam.ac.uk/~amp12/freshml/ . They are also called nomes.

If you have a system that is strong enough to know that (+) is  
commutative,
then nominal unification should be able to prove the equivalence of

template<int I, int J> void f(int (&array)[J+I]);
template<int X, int Y> void f(int (&array)[X+Y]);

But, do we want a theorem prover in clang? ;-)

Cheers,

	Gabor