termination for FDs and ATs

[Ross Paterson]

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.