[Haskell-cafe] Strange error with type classes + associated types
byorgey at seas.upenn.edu
Wed Apr 14 10:30:08 EDT 2010
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
> :: (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),
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...
> 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.
More information about the Haskell-Cafe