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

[Brent Yorgey]

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

The type of a2 is unified with (v :-* w) and the type of a1 is unified
with (u :-* v).  Since both a1 and a2 are obtained from
pattern-matching on an Affine constructor (which contains something of
type (z :-* z)), u, v, and w ought to all unify to the same thing.
Instead we get a bunch of strange type equalities which don't help
because Scalar and Basis may not be injective.

> 
> If you add that type back to the file containing append it no longer
> type checks...
> 
> VectorSpaceTest.hs:44:54:
>     Couldn't match expected type `Basis u'
>            against inferred type `Basis u1'
>       NB: `Basis' is a type function, and may not be injective
>       Expected type: u :-* v
>       Inferred type: v :-* v
>     In the second argument of `(*.*)', namely `a1'
>     In the first argument of `Affine', namely `(a2 *.* a1)'
> Failed, modules loaded: none.
> 
> [ It also has the problem that its type isn't compatible with monoidal
> mappend anyway ]

Its type WOULD be compatible with mappend (just unify v and v1) if it
weren't for that pesky u.

Thanks for looking at this.  I think I'll file a bug.  I hope very
much that it IS a bug, because otherwise I don't understand what's
going on at all.

-Brent