implicit search should more uniformally carry constraints through chained conversions/searches

[scabug]

1. implicit search and implicit conversion search treat undetermined type parameters differently
2. constraints are carried over in an ad-hoc way (by tracking undetermined type parameters in the context)
   --> this works for influencing the inference of type parameters by "later aspects" of the expression, but not for inferring implicit values, since these cannot be left undetermined while type checking an expression (see [#SI-4653])

the idea of generalising tracking of undetermined implicit types (type parameters)/implicit values and their constraints could drive the solution for [SI-3340], [SI-3346], [SI-2781] and [SI-3270]

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-4699?orig=1
Reporter: @adriaanm
Blocks #5107, #2673, #3270, #4653, #3340, #5592, #3346, #2781

[scabug]

@Blaisorblade said:
I was wondering: can available implicits be modeled as constraints? Also, could constraint solving be done once per statement, instead of on each invocation (as currently specified)?

The more I run into problems, the more it seems that even more should be delegated to a constraint solver (see also #5298).

[scabug]

@paulp said:
I've always thought we should be using a separate solver, but I might be biased because it'd be that much less code for me to manage.

[scabug]

@dcsobral said:
I think using constraint solvers takes advantage of a lot of work that have been done to make them fast, makes it easier to produce a formal specification for it, and easier to change the knobs.

Then again, I don't even know what's underneath, so I might be completely off and this comment just noise.

[scabug]

@paulp said:
I know what's underneath (on the scala side - I don't know what's underneath the constraint solvers) and if anything you understate the advantages.

[scabug]

@Blaisorblade said:
I think that writing (and publishing) an implementable and reasonable formal specification has an even bigger advantage: you need to make it understandable and regular (which benefits users). To fix a bug like #5298, you just need to translate bounds to constraints directly; with an ideal proof of "completeness", such a bug would likely be impossible by design, although existing completeness proofs for local type inference systems seem to often have various restrictions. The only obstacle is that defining the formalization risks being extremely complicated - I think it could even be enough for a PhD thesis.

But wasn't Hubert Plociniczak, PhD candidate, planning to use constraint solving to improve both Scala type inference and for the type debugger [1], based on research by Martin Odersky et al. on one side, and GHC hackers on the other? He also gives a number of convincing arguments on why one should use constraint systems. Among others, it's easier to explain type inference errors in terms of constraints.

Of course research proposals for PhD students are not binding - my research proposal had absolutely no relevance (I'm a PhD student). A lot of disclaimers apply for me too: my knowledge of type inference goes barely beyond Pierce's TAPL book, and I've only skimmed his research proposal (too hard for me, sorry).

[1] Hubert Plociniczak, 2010. Making sense out of an advanced type system. Edic research proposal. Available at
http://wiki.epfl.ch/edicpublic/documents/Candidacy%20exam/hubert_plociniczak_candidacy.pdf

[scabug]

@adriaanm said:
Unassigning as milestone deadline was reached.

[scabug]

@adriaanm said:
fixed as part of #3346