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 <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
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe