(j3.2006) more on J32031 equivalence of circular types

[Van Snyder]

On Wed, 2008-08-20 at 15:19 -0700, Aleksandar Donev wrote:
> On Wednesday 20 August 2008 15:15, Bill Long wrote:
> > I guess I don't see what part of the answer is not obvious here.  What
> > part of f03:4.5.1.3 is ambiguous in the case?
> 
> TYPE(T), POINTER :: NEXT => NULL()
> 
> Does this component in type T in module FOO have the same type as that in 
> module BAR? If you know the answer, you've already answered the question you 
> are trying to answer. You get into an infinite loop that you must terminate 
> somehow.

The answer depends upon whether you start by assuming the types are
equivalent and try to prove they're not, or start by assuming the types
are different and try to prove they're equivalent.

In the first case, you assume the types of A and B are equivalent.  Then
you start doing a simultaneous recursive traversal of both type systems'
graphs (type systems in the case of recursive types involving more than
one type).  When you arrive at types you've visited, you say "Aha! I've
been here, so they must be the same!"  If you arrive at anything
different in the traversals, you quit and say "No!"  If you finish
traversing the graphs by visiting every vertex without saying "No!", you
quit and say "Yes!"

Mike gets into an infinite loop by assuming the types of A and B are not
equivalent, so when he arrives at TYPE(T), POINTER :: NEXT he knows he's
been there, but not that the T's are equivalent, so he dives into their
graphs.