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

[Ryan Ingram]

On Mon, Apr 6, 2009 at 2:36 PM, Peter Berry <pwberry at gmail.com> wrote:
> 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