[Haskell-cafe] Re: Associated Type Synonyms question

[Ross Paterson]

On Fri, Feb 17, 2006 at 01:26:18PM +0000, Stefan Wehr wrote:
> Martin Sulzmann <sulzmann at comp.nus.edu.sg> wrote::
> > By possible you mean this extension won't break any
> > of the existing ATS inference results?
> 
> Yes, although we didn't go through all the proofs.
> 
> > You have to be very careful otherwise you'll loose decidability.

The paper doesn't claim a proof of decidability (or principal types),
but conjectures that it will go through.

Apropos of that, I tried translating the non-terminating FD example from
the FD-CHR paper (ex. 6) to associated type synonyms (simplified a bit):

	data T a = K a;

	class C a where {
		type S a;
		r :: a -> S a;
	}

	instance C a => C (T a) where {
		type S (T a) = T (S a);
		r (K x) = K (r x);
	}

	f b x = if b then r (K x) else x;

Phrac infers

	f :: forall a . (S (T a) = a, C a) => Bool -> a -> T (S a)

The constraint is reducible (ad infinitum), but Phrac defers constraint
reduction until it is forced (as GHC does with ordinary instance
inference).  We can try to force it using the MR, by changing the
definition of f to

	f = \ b x -> if b then r (K x) else x;

For this to be legal, the constraint must be provable.  In the
corresponding FD case, this sends GHC down the infinite chain of
reductions, but Phrac just gives up and complains about deferred
constraints being left over after type inference.  I don't think this
is right either, as in other cases the constraint will reduce away
to nothing.