[Haskell-cafe] Re: Small displeasure with associated type synonyms

[Tom Schrijvers]

> I don't see how your example explains this particular error.
> I agree Int cannot be generalized to (T Int) or (T Bool).

Generalized is not the right word here. In my example T Int, T Bool and 
Int are all equivalent.

> I see Stefan's local type signature is not (val :: a) like your (val ::Int) 
> but (val :: T a) which is a whole different beast.

Not all that different. As in my example the types T Int, T Bool and Int 
are equivalent, whether one writes val :: Int, val :: T Int or val :: T 
Bool. My point is that writing val :: T Int or val :: T Bool does not help 
determining whether one should pick the val implementation of instance C 
Int or C Bool.

> And (T a) is the type that ghc should assign here.

As my example tries to point out, there is not one single syntactic form 
to denote a type.

Consider the val of in the first component. Because of val's signature in 
the type class the type checker infers that the val expression has a type 
equivalent to T a2 for some a2. The type checker also expects a type 
equivalent to T a, either because of the type annotation or because of the 
left hand side. So the type checker must solve the equation T a ~ T a2 for 
some as yet to determine type a2 (a unification variable). This is 
precisely where the ambiguity comes in. The type constructor T is not 
injective. That means that the equation may hold for more than one value 
of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type 
checker complains:

 	Couldn't match expected type `T a2' against inferred type `T a'.

Maybe you don't care what type is chosen, if multiple ones are possible. 
My example tried to show that this can effect the values computed by your 
program. So it does matter.

For this particular example, it seems that the type checker does not have 
have more than alternative for a2 in scope. However, it is not aware of 
that fact. It uniformly applies the same general strategy for solving 
equations in all contexts. This is a trade-off in type system complexity 
vs. expressivity.

There is an opportunity for exploring another point in the design space 
here.

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/