termination for FDs and ATs

[Martin Sulzmann]

Ross Paterson writes:
 > On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
 > > Yes, FDs and ATs have the exact same problems when it comes to termination.
 > > The difference is that ATs impose a dynamic check (the occurs check)
 > > when performing type inference (fyi, such a dynamic check is sketched
 > > in a TR version of the FD-CHR paper).
 > 
 > Isn't an occurs check unsafe when the term contains functions (type
 > synonyms)?  You might reject something that would have been accepted
 > if the function had been reduced and discarded the problematic subterm.
 > 

Correct. Any dynamic check is necessarily incomplete.

Martin