On Mon, Apr 6, 2009 at 2:36 PM, Peter Berry
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
This isn't true, though, and for similar reasons why you can't declare a generic "instance Fun d => Functor (Memo d)". Type synonyms are not injective; you can have two instances that point at the same type: data Unit1 = Unit1 data Unit2 = Unit2 newtype Identity x = Id x unit_abst x f = Id (f x) unit_appl (Id v) _ = v instance Fun Unit1 where type Memo Unit1 = Identity abst = unit_abst Unit1 appl = unit_appl instance Fun Unit2 where type Memo Unit2 = Identity abst = unit_abst Unit2 appl = unit_appl Now, Memo Unit1 a = Identity a = Memo Unit2 a, but that does not give us that Unit1 = Unit2. In fact, memo_fmap' is ambiguous; what should this application do? memo_fmap' id (Id ()) Should it look at the instance for Unit1, or Unit2, or some other instance we haven't given yet? You can use a data family instead, and then you get the property you want; if you make Memo a data family, then Memo d1 = Memo d2 does indeed give you d1 = d2. You can still use other types in your instances, just use "newtype instance Memo Unit1 a = MemoUnit1 (Identity a)" and add the appropriate newtype wrappers and unwrappers.
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)
Right, because now you have constrained appl ahead of time, passing in the correct type, instead of hoping the compiler can guess how you meant to use "appl". I don't know if this function is callable, though; at the very least you need to annotate its call site to get the proper instance passed through. This is somewhat solvable with a proxy element to fix the instance of Fun: data Proxy d = Proxy memo_fmap_nonamb :: Fun d => Proxy d -> (a -> b) -> Memo d a -> Memo d b memo_fmap_nonamb _ f x = abst (f . appl x) I don't know if this version compiles without the type annotation; my guess is that it might! But even if it doesn't, once you add the proper annotation it is at least callable: test = memo_fmap_nonamb (Proxy :: Proxy Unit1) id (Id ()) I think, for this problem, data families are a better solution. They also let you write the generic Functor instance. -- ryan