TDNR without new operators or syntax changes

[Dan Doel]

On Thu, May 26, 2016 at 5:14 AM, Peter <voldermort at hotmail.com> wrote:
> Solving for everything but f, we get f :: T -> Int.

So TDNR happens for things in function position (applied to something).

> Solving for everything but f, we get f :: T -> Int.

So TDNR happens for things in argument position.

> May not be solvable, would fail to disambiguate.

But there's exactly one combination of f and v definitions that will
succeed with the right type. So why doesn't that happen? Here's an
intermediate step:

    i1' x = f x :: Int

What happens there? Another way to phrase the question is: why would
TDNR only disambiguate based on argument types of functions and not on
return types? Why would function types even be a factor at all?

And to be honest, I don't really think the description of what the
type checker would be doing is detailed enough. If there are two
ambiguous candidates how does type checking proceed with 'the type in
the declared signature' when there are two possible signatures which
may be completely different? Is it doing backtracking search? How do
you add backtracking search to GHC's inference algorithm? Etc. The
later examples are designed to raise questions about this, too.

I'm rather of the opinion that TDNR just isn't a good feature for most
things. Implicit in the famous "How to Make Ad-hoc Polymorphism Less
Ad-hoc" is that being ad-hoc is bad. And type classes fix that by
turning overloading into something that happens via an agreed upon
interface, with declared conventions, and which can be abstracted over
well. But TDNR has none of that, so to my mind, it's not really
desirable, except possibly in cases where there is no hope of being
abstract (for instance, Agda does some TDNR for constructors in
patterns, and there isn't much basis in the underlying theory for
trying to abstract over doing induction on completely different types
with similarly named pieces; so it's more acceptable).

But also, for something as far reaching as doing TDNR for every
ambiguous name, it's not terribly clear to me what a good algorithm
even is, unless it's only good enough to handle really simple
examples, and just doesn't work most of the time (and even then, I'm
not sure it's been thought through enough to say that it's a simple
addition to GHC's type checking).

-- Dan