[Haskell-cafe] Strange type error with associated type synonyms

[Peter Berry]

> {-# LANGUAGE TypeFamilies, TypeSynonymInstances, ScopedTypeVariables #-}

The following is a class of memo tries indexed by d:

> class Fun d where
>     type Memo d :: * -> *
>     abst :: (d -> a) -> Memo d a
>     appl :: Memo d a -> (d -> a)
>     -- Law: abst . appl = id
>     -- Law: appl . abst = id (denotationally)

Any such type Memo d is naturally a functor:

> memo_fmap f x = abst (f . appl x)

The type of memo_fmap (as given by ghci) is (Fun d) => (a -> c) ->
Memo d a -> Memo d c. (Obviously this would also be the type of fmap
for Memo d, so we could declare a Functor instance in principle.) If
we add this signature:

> memo_fmap' :: Fun d => (a -> b) -> Memo d a -> Memo d b
> memo_fmap' f x = abst (f . appl x)

it doesn't type check:

TypeSynonymTest.hs:14:17:
    Couldn't match expected type `Memo d1 b'
           against inferred type `Memo d b'
    In the expression: abst (f . appl x)
    In the definition of `memo_fmap'':
        memo_fmap' f x = abst (f . appl x)

TypeSynonymTest.hs:14:32:
    Couldn't match expected type `Memo d a'
           against inferred type `Memo d1 a'
    In the first argument of `appl', namely `x'
    In the second argument of `(.)', namely `appl x'
    In the first argument of `abst', namely `(f . appl x)'
Failed, modules loaded: none.

As I understand it, the type checker's thought process should be along
these lines:

1) the type signature dictates that x has type Memo d a.
2) appl has type Memo d1 a -> d1 -> a for some d1.
3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1

But for some reason, step 3 fails. If we annotate appl with the
correct type (using scoped type variables), it type checks:

> -- thanks to mmorrow on #haskell for this
> memo_fmap'' :: forall a b d. Fun d => (a -> b) -> Memo d a -> Memo d b
> memo_fmap'' f x = abst (f . (appl :: Memo d a -> d -> a) x)

My ghc is 6.8.2, but apparently this happens in 6.10 as well.

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html