Thanks for clarifying this. On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote:
So, we get the following type for f
f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]
Given the instance definitions of that example, you can never satisfy the equality [Result a b] = b, and hence, never apply the function f.
That would be the case if the definition were f b x y = if b then x .*. [y] else y You'd assign f a type with unsatisfiable constraints, obtaining termination by deferring the check. But the definition f = \ b x y -> if b then x .*. [y] else y will presumably be rejected, because you won't infer the empty context that the monomorphism restriction demands. So the MR raises the reverse question: can you be sure that every tautologous constraint is reducible?
So, clearly termination for ATs and FDs is *not* the same. It's quite interesting to have a close look at where the difference comes from. The FD context corresponding to (*) above is
Mul a [b] b
Improvement gives us
Mul a [[c]] [c] with b = [c]
which simplifies to
Mul a [c] c
which is where we loop. The culprit is really the new type variable c, which we introduce to represent the "result" of the type function encoded by the type relation Mul. So, this type variable is an artifact of the relational encoding of what really is a function,
It's an artifact of the instance improvement rule, but one could define a variant of FDs without that rule. Similarly one could have a variant of ATs that would attempt to solve the equation [Result a b] = b by setting b = [c] for a fresh variable c. In both cases there is the same choice: defer reduction or try for more precise types at the risk of non-termination for instances like these.