[Haskell-cafe] Strange error with type classes + associated types

[Roman Leshchinskiy]

On 15/04/2010, at 00:30, Brent Yorgey wrote:

> On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote:
>> On 14 April 2010 03:48, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
>> 
>>> Can someone more well-versed in the intricacies of type checking with
>>> associated types explain this?  Or is this a bug in GHC?
>> 
>> If you take the definition of append out out the class - GHCi will
>> give it a type:
>> 
>>> append (Affine a2 b2) (Affine a1 b1) = Affine (a2 *.* a1) (lapply a2 b1 ^+^ b2)
>> 
>> *VectorSpace> :t append
>> append
>>  :: (Scalar v ~ Scalar v1,
>>      Basis v ~ Basis u,
>>      Basis v1 ~ Basis v,
>>      VectorSpace v1,
>>      HasTrie (Basis v),
>>      HasBasis v,
>>      HasBasis u) =>
>>     Affine v1 -> Affine v -> Affine v1
> 
> Right, this seems weird to me.  Why is there still a 'u' mentioned in
> the constraints?  Actually, I don't even see why there ought to be
> both v and v1.  The type of (*.*) mentions three type variables, u, v, and w:
> 
> (*.*)  :: (HasBasis  u, HasTrie  (Basis  u), 
>           HasBasis  v, HasTrie  (Basis  v), 
>           VectorSpace  w, 
>           Scalar  v ~ Scalar  w) 
>       => (v :-*  w) -> (u :-*  v) -> u :-*  w

Note that (:-*) is a type synonym:

type :-* u v = MSum (Basis u :->: v)

Substituting this into the type of (*.*), we get:

(*.*) :: ... => MSum (Basis v :-* w) -> MSum (Basis u :-* v) -> MSum (Basis u :-* w)

Now, Basis is an associated type:

class VectorSpace v => HasBasis v where
  type Basis v
  ...

This means that there is no way to obtain u from Basis u. Since u only ever occurs as an argument to Basis, a type family, it can never be unified with anything. This, in turn, means that there is no way to call (*.*) at all (unless I'm severely mistaken).

Roman