Quantified constraint trick

DG.hs

{-# LANGUAGE
    ConstraintKinds,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    QuantifiedConstraints,
    RankNTypes,
    ScopedTypeVariables,
    TypeApplications,
    UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-simplifiable-class-constraints #-}
module DG where

import GHC.Generics

class RepBimap a a' b b' rep rep' where
  repBimap :: (a -> a') -> (b -> b') -> rep -> rep'

gbimap :: forall f a a' b b'. GBimap f => (a -> a') -> (b -> b') -> f a b -> f a' b'
gbimap f g =
  with @(RepBimapRep a a' b b' f)   -- Not needed since GHC 9.2
    (to @_ @() . repBimap f g . from @_ @())

with :: forall c r. (c => r) -> (c => r)
with x = x

class    (forall a b. Generic (f a b), forall a a' b b'. RepBimapRep a a' b b' f) => GBimap f
instance (forall a b. Generic (f a b), forall a a' b b'. RepBimapRep a a' b b' f) => GBimap f

class    RepBimap a a' b b' (Rep (f a b) ()) (Rep (f a' b') ()) => RepBimapRep a a' b b' f
instance RepBimap a a' b b' (Rep (f a b) ()) (Rep (f a' b') ()) => RepBimapRep a a' b b' f