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). A problem with ATs at the moment is that some terminating FD programs result into non-terminating AT programs. Somebody asked how to write the MonadReader class with ATs: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html This requires an AT extension which may lead to undecidable type inference: http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html Martin Ross Paterson writes:
To ensure termination with FDs, there is a proposed restriction that an instance that violates the coverage condition must have a trivial instance improvement rule. Is the corresponding restriction also required for ATs, namely that an associated type synonym definition may only contain another associated type synonym at the outermost level? If not, wouldn't the non-terminating example from the FD-CHR paper (ex. 6, adapted below) also be a problem for ATs?
class Mul a b where type Result a b (.*.) :: a -> b -> Result a b
instance Mul a b => Mul a [b] where type Result a b = [Result a b] x .*. ys = map (x .*.) ys
f = \ b x y -> if b then x .*. [y] else y
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime