On Wed, Apr 14, 2010 at 09:51:52AM +0100, Stephen Tetley wrote: > On 14 April 2010 03:48, Brent Yorgey <byor...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe