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 _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime