Reasoning about AllZip and AllZip2

[edsko]

Motivation

Not sure where this belongs, and in exactly what shape, but I had a class

class Annotate' a b where
  annotate'       :: a -> b
  dropAnnotation' :: b -> a

for which I support generic deriving:

instance ( SOP.Generic a
         , SOP.Generic b
         , SOP.AllZip2 Annotate' (SOP.Code a) (SOP.Code b)
         ) => CanAnnotate (AnnotateGenericallyAs b a) where

The dropAnnotation' case is awkward however, because we know SOP.AllZip2 Annotate' (SOP.Code a) (SOP.Code b), but we need something that relates SOP.Code b and SOP.Code a (rather than the other way around). In the end I wrote the below; perhaps we could/should give this a place in the lib somewhere?

Code

class    c y x => Inv (c :: l -> k -> Constraint) (x :: k) (y :: l)
instance c y x => Inv (c :: l -> k -> Constraint) (x :: k) (y :: l)

data Dict2 (c :: k -> k -> Constraint) (x :: k) (y :: k) where
  Dict2 :: c x y => Dict2 c x y

invZip :: forall k c (xs :: [k]) (ys :: [k]).
     SOP.AllZip c xs ys
  => Proxy c
  -> Proxy ys
  -> Proxy xs
  -> Dict2 (SOP.AllZip (Inv c)) ys xs
invZip _ _ _ = go SOP.shape SOP.shape
  where
    go :: forall xs' ys'.
         SOP.AllZip c xs' ys'
      => SOP.Shape xs' -> SOP.Shape ys' -> Dict2 (SOP.AllZip (Inv c)) ys' xs'
    go SOP.ShapeNil        SOP.ShapeNil      = Dict2
    go (SOP.ShapeCons xs) (SOP.ShapeCons ys) =
        case go xs ys of
          Dict2 -> Dict2

zipImplies :: forall k c d (xs :: [k])  (ys :: [k]).
      SOP.AllZip c xs ys
   => Proxy c
   -> Proxy d
   -> Proxy xs
   -> Proxy ys
   -> (forall x y. c x y => Proxy x -> Proxy y -> Dict2 d x y)
   -> Dict2 (SOP.AllZip d) xs ys
zipImplies _ _ _ _ f = go SOP.shape SOP.shape
  where
    go :: forall xs' ys'.
         SOP.AllZip c xs' ys'
      => SOP.Shape xs' -> SOP.Shape ys' -> Dict2 (SOP.AllZip d) xs' ys'
    go SOP.ShapeNil        SOP.ShapeNil      = Dict2
    go (SOP.ShapeCons xs) (SOP.ShapeCons ys) =
        case (f (Proxy @(SOP.Head xs')) (Proxy @(SOP.Head ys')), go xs ys) of
          (Dict2, Dict2) -> Dict2

invAllZip :: forall k (c :: k -> k -> Constraint) (xss :: [[k]]) (yss :: [[k]]).
     SOP.AllZip (Inv (SOP.AllZip c)) xss yss
  => Proxy c
  -> Proxy xss
  -> Proxy yss
  -> Dict2 (SOP.AllZip (SOP.AllZip (Inv c))) xss yss
invAllZip pc pxss pyss =
    zipImplies
      (Proxy @(Inv (SOP.AllZip c)))
      (Proxy @(SOP.AllZip (Inv c)))
      pxss
      pyss
      (invZip pc)

invZip2 :: forall k c (xss :: [[k]]) (yss :: [[k]]).
     SOP.AllZip2 c xss yss
  => Proxy c
  -> Proxy yss
  -> Proxy xss
  -> Dict2 (SOP.AllZip2 (Inv c)) yss xss
invZip2 pc pyss pxss =
    case invZip (Proxy @(SOP.AllZip c)) pyss pxss of
      Dict2 -> case invAllZip pc pyss pxss of
                 Dict2 -> Dict2

htransInv_SOP :: forall k c f g (xss :: [[k]]) (yss :: [[k]]).
     SOP.AllZip2 c yss xss
  => Proxy c
  -> (forall x y. c y x => f x -> g y)
  -> SOP f xss
  -> SOP g yss
htransInv_SOP pc f =
    case invZip2 pc (Proxy @xss) (Proxy @yss) of
      Dict2 -> SOP.htrans (Proxy @(Inv c)) f