content: {-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}
  
  module T3330c where
  
  import Data.Kind
  
  data (f :+: g) x = Inl (f x) | Inr (g x)
  
  data R :: (Type -> Type) -> Type where
    RSum  :: R f -> R g -> R (f :+: g)
  
  class Rep f where
    rep :: R f
  
  instance (Rep f, Rep g) => Rep (f :+: g) where
    rep = RSum rep rep
  
  type family Der (f :: Type -> Type) :: Type -> Type
  type instance Der (f :+: g) = Der f :+: Der g
  
  plug :: Rep f => Der f x -> x -> f x
  plug = plug' rep where
  
  plug' :: R f -> Der f x -> x -> f x
  plug' (RSum rf rg) (Inl df) x = Inl (plug rf df x)
  
  {-
  rf :: R f1, rg :: R g1
  Given by GADT match: f ~ f1 :+: g1
  
  Second arg has type (Der f x)
      = (Der (f1:+:g1) x)
      = (:+:) (Der f1) (Der g1) x
  Hence df :: Der f1 x
  
  Inl {f3,g3,x} (plug {f2,x1} rf df x)  gives rise to
    result of Inl:   ((:+:) f3 g3 x ~ f x)
    first arg (rf):  (R f1 ~ Der f2 x1)
    second arg (df): (Der f1 x ~ x1)
    result of plug:  (f2 x1 ~ x -> f3 x)
  
    result of Inl: ((:+:) f3 g3 x ~ f x)
         by given  ((:+:) f3 g3 x ~ (:+:) f1 g1 x)
    hence need f3~f1, g3~g1
  
  So we are left with
     first arg:      (R f1 ~ Der f2 x1)
     second arg:     (Der f1 x ~ x1)
     result:         (f2 x1  ~  (->) x (f3 x))
  
  Decompose result:
            f2 ~ (->) x
            x1 ~ f1 x
  Hence
          first:  R f1 ~ Der ((->) x) (f1 x)
    decompose  : R ~ Der ((->) x)
                 f1 ~ f1 x
  
  
  -}
  