On Thu, Mar 6, 2008 at 7:16 PM, Luke Palmer
I agree that this would be nice. But I think that the situation is stickier than it looks on the surface. Consider this:
instances GShow [a] where instance [Char] where gShow = id instance [a] where gShow x = "list(" ++ length x ++ ")"
gShow' :: [a] -> String gShow' = gShow
I'm not so sure. It's not that hard to imagine a compiler where the core-language expansion of this code looks like this: data GShowDict a = GShowDict { gShow :: a -> String } id :: (a :: *) -> a -> a id A a = a length :: (a :: *) -> [a] -> Int -- definition elided gShow' :: (a :: *) -> [a] -> String gShow' A = gShow (mkDict_GShow_List A) mkDict_GShow_List :: (a :: *) -> GShowDict [a] mkDict_GShow_List A = typecase A of Char -> GShowDict (id [A]) _ -> GShowDict (\xs -> length A xs) Now, it's true that this means that you can no longer do full type erasure, but I'm not convinced of the importance of that anyways; if you look at mainstream languages you generally only get type erasure for a restricted subset of the types and that's good enough for performance: 1) In Java, you only get type erasure for primitive types; everything else needs its type tag so it can be safely downcasted from Object. 2) In C++ only primitive types and structs/classes with no virtual functions get type erasure; if a class has virtual functions its virtual function table is implicitly a "type tag". I don't think the cost is that great; the compiler can easily flag polymorphic functions that require type information for some or all arguments and in many cases the type evidence can be passed "just-in-time" when calling from a non-polymorphic function into a polymorphic function.
When we get to more complex examples like the one you gave above involving constraints, in order to solve for the constraints needed for an instance of C [a] you need a *disjunction* constraint, which vastly increases the likelihood of an undecidable solution.
This is definitely an issue. I don't have a full understanding of the methods used for typechecking/inference of typeclasses; I'm just a programmer who wants MORE POWER :) -- ryan