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

14 Apr 2010

      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  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

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

Roman Leshchinskiy