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