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

14 Apr 2010

      On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote:
...
On 14 April 2010 03:48, Brent Yorgey  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