[Haskell-cafe] Use distributivity proof in a simple example

[Marco Vassena]

My GADT data type is indexed over type level list.

data DF (xs :: [ * ]) where
	Empty :: DF []
	Single :: a -> DF '[ a ]
	Cons :: DF xs -> DF ys -> DF (Append xs ys)

Append is a type family that append two type level lists:
type family Append (xs :: [ * ]) (ys :: [ * ]) :: [ * ] where
 Append '[] ys = ys
 Append (x ': xs) ys = x ': Append xs ys

Map is a type level map:
type family Map (f :: * -> *) (xs :: [ * ]) :: [ * ] where
 Map f '[] = '[] 
 Map f (x ': xs) = f x ': Map f xs

Now I want to write a function that wraps all the component in Single in a list:
wrap :: DF xs -> DF (Map [] xs)
wrap Empty = Empty
wrap (Single a) = Single [ a ]
wrap (Cons x y) = Cons (wrap x) (wrap y) -- Type Error 

The type-checker doesn't know anything about distributivity:
Could not deduce (Append (Map [] xs) (Map [] ys) ~ Map [] zs)
   from the context (zs ~ Append xs ys)

I managed to prove this property by induction on the first type level list.

class MapDist xs where
 mapDist :: (zs ~ Append xs ys) => Proxy xs -> Proxy ys -> Append (Map [] xs) (Map [] ys) :~: Map [] zs

instance MapDist '[] where
 mapDist Proxy Proxy = Refl

tailP :: Proxy (x ': xs) -> Proxy xs
tailP _ = Proxy

instance MapDist xs => MapDist (x ': xs) where
 mapDist p1 p2 = 
   case mapDist (tailP p1) p2 of
     Refl -> Refl

I have adjusted wrap as follows:

toProxy :: DataFormat xs -> Proxy xs
toProxy _ = Proxy

wrap (Cons x y) = 
 let p1 = toProxy x
     p2 = toProxy y in
 case mapDist p1 p2 of
   Refl -> Cons (wrap x) (wrap y) 

The problem now is that MapDist xs is not in the context.
Adding it to the Cons constructor in the GADT definition does not solve the problem:
	Could not deduce (MapDist (Map [] xs)) ...

How can I solve this issue?
Clearly the two instances of MapDist cover all possible cases, and therefore it should be possible
to use it for any list xs.

I tried avoiding the type class MapDist with a normal function:
proof :: forall xs ys zs . Append xs ys ~ zs => 
 Proxy xs -> Proxy ys -> Proxy zs -> 
 Append (Map [] xs) (Map [] ys) :~: Map [] zs

However here I have no mean to distinguish the base case ('[]) from
the inductive case (x ': xs), thus I cannot complete the proof.

Do you have any idea, suggestion or workaround for this kind of situations?

Cheers,
Marco