[SI2712] implement higherorder unification for type constructor inference Created: 27/Nov/09 Updated: 18/Oct/16 Resolved: 27/May/16 

Status:  CLOSED 
Project:  Scala Programming Language 
Component/s:  Compiler (Misc) 
Affects Version/s:  None 
Fix Version/s:  Scala 2.11.9, Scala 2.12.0M5 
Type:  Improvement  Priority:  Minor 
Reporter:  Adriaan Moors  Assignee:  Adriaan Moors 
Resolution:  Fixed  Votes:  83 
Labels:  None  
Environment: 
tcpoly_infer 
Issue Links: 


TracCC: 
Alan, arjan blokzijl, Christos KK Loverdos, Eric Torreborre, Evgeny, Ismael Juma, Ittay Dror, Johannes Rudolph, Jorge Ortiz, Josh Suereth, Kris Nuttycombe, Mark Harrah, Michael, Miles Sabin, Nick Partridge, Seth Tisue, Tony Morris, weihsiu

Description 
implement what's described in "Partial polymorphic type inference and higherorder unification"

Comments 
Comment by Harrison Klaperman [ 05/Jun/11 ]  
You can find that paper here: http://www.cs.cmu.edu/~fp/papers/lfp88.pdf. I hope this is useful to others who stumble upon this issue. Now if only I understood what the paper were talking about...  
Comment by Paolo G. Giarrusso [ 19/Oct/11 ]  
Further work on that problem is described in "Unification via explicit substitutions: The case of higherorder patterns"  http://www.cs.cmu.edu/~fp/papers/INRIARR3591.pdf, from Dowek, Hardin, Kirchner and Pfenning (Pfenning is the author of the above paper). I am not an expert, but this work is cited in Pierce's TAPL (Sec. 23.6, pag. 355), which explains that unlike the algorithm above it is terminating and always finds a unique solution; the paper suggests that this work applies to an important subcase. However, I cannot fully judge myself the respective merits of the two papers.  
Comment by Miles Sabin [ 06/Nov/11 ]  
With dependent method types we have a somewhat cumbersome, but just about usable workaround. The key idea is to use implicits to destructure a type, and then pick out and use its component parts as dependent types.
See also here for a slightly more elaborate scalaz inspired example.  
Comment by Paolo G. Giarrusso [ 09/Dec/11 ]  
Milles Sabin, your workaround is interesting: type EitherInt[A] = Either[Int, A] Moreover, your code does not even correctly solve the original problem  it only infers that Int => Int matches M0[A0, B0] with M0 = Function1, not that it matches M1[A1] with M1[X] = X => X.  
Comment by Jason Zaugg [ 02/Dec/12 ]  
See also  
Comment by Paul Chiusano [ 02/Dec/12 ]  
Would it be any easier to just look for partial applications of existing type constructors in lefttoright order? Haskell does roughly this (actually, type constructors are just curried, see below), it is tractable, and people don't seem to have an issue with the limitation, though occasionally you do have to introduce a new type just to flip the order of some type parameters. Here's an example:
Another way to think about this is that type constructors are curried, so State[S,A] is actually represented as Ap(Ap(State, S), A), and likewise the M[A] is Ap(freevar, A)  these unify with freevar = Ap(State, S).  
Comment by Dan Rosen [ 19/Apr/13 ]  
To Paul's comment, I agree that looking at the type parameters as curried, partially applied from left to right (SI4719) is probably usually good enough. If State[S, A] has pseudoHaskellish kind (*, *) > *, then State[S][A] would have kind * > * > *, and State[S] would have kind * > *.  
Comment by Paolo G. Giarrusso [ 17/Sep/14 ]  
It seems somehow I never mentioned higherorder pattern unification by Miller, which is what Agda uses — the paper I linked ("Unification via explicit substitutions: The case of higherorder patterns") is indeed about that. For whatever reason, everybody steers away from the original Huet algorithm, including modern implementation of lambdaProlog (which is what "Partial Polymorphic Type Inference and HigherOrder Unification" uses).  
Comment by Adriaan Moors [ 30/Jun/15 ]  
Oh, jira.  
Comment by Seth Tisue [ 30/Jun/15 ]  
 
Comment by Miles Sabin [ 01/Jul/15 ]  
That was cruel and heartless ...  
Comment by Eric Torreborre [ 01/Jul/15 ]  
My heart rate went up for a moment...  
Comment by Stephen Compall [ 01/Jul/15 ]  
long, wistful sigh  
Comment by Jed WesleySmith [ 01/Jul/15 ]  
well, that was (briefly) exciting!  
Comment by Matthew Pocock [ 23/Jul/15 ]  
I keep on hitting this issue in various forms, most recently when trying to use type lambdas to fill in one of two types on a * > * > * kinded type. I have this type: ``` object RangeAs { } There are various implicit instances with RangeAs.Aux[X]#l as one of their type parameters. They are not found in all situations if I attempt to summon them using the lambda. However, if I do this: ``` Now if I summon them using RangeAsX, they are found.  
Comment by Ismael Juma [ 12/Apr/16 ]  
For the watchers of this JIRA that haven't seen this on Twitter, Miles posted a demo project exercising a proposed fix for this JIRA:  
Comment by Miles Sabin [ 15/Apr/16 ]  
PR against 2.12.x here: https://github.com/scala/scala/pull/5102.  
Comment by Miles Sabin [ 26/Aug/16 ]  
Backport to 2.11.8 available here.  
Comment by Adriaan Moors [ 18/Oct/16 ]  
2.11.9 PR: https://github.com/scala/scala/pull/5343 