There is a general solution, but it essentially involves polymorphism a-la-Omega (or as in Coq's Calculus of Inductive Constructions). The most general description of (Tree Int) is as the Stream S = [Int, Tree, Id, Id, ...] You are now attempting to pull-off exactly 2 "terms" from that Stream. The solutions are: 0: Int, Tree 1: Tree Int, Id 2: Id (Tree Int), Id 3: Id (Id (Tree Int)), Id Let T@i denote n-ary type-level application, where T is a list of types, and i>=0. Consider the pair ( S!!(i+1), (take i S)@i) This is the /closed-form/ for the n'th solution (m, a) for unifying (m a) with (Tree Int). A better way to _represent_ this closed form is as (S, i) where S = [Int,Tree, Id, Id, ...] from which further constraints can decide what is the 'proper' value of i to take. This even shows how to do defaulting: in the absence of further information, take the smallest i possible. [I phrase it this way because there are times where constraints will force a certain minimum on i, but no maximum]. In other words, the above should be backwards compatible with current behaviour, since the 'default' solution would be m=Tree, a=Int. Jacques Simon Peyton-Jones wrote:
I remember that I have, more than once, devoted an hour or two to the question "could one add Id as a distinguished type constructor to Haskell". Sadly, each time I concluded "no".
I'm prepared to be proved wrong. But here's the difficulty. Suppose we want to unify (m a) with (Tree Int)
At the moment there's no problem: m=Tree, a=Int. But with Id another solution is m=Id, a=Tree Int
And there are more m=Id, a=Id (Tree Int)
We don't know which one to use until we see all the *other* uses of 'm' and 'a'.
I have no clue how to solve this problem. Maybe someone else does. I agree that Id alone would be Jolly Useful, even without full type-level lambdas.
Simon _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime