post correspondence problem in djinn env, assuming that recursive data types are allowed

Djinn-env

-- a djinn environment that encodes an instance of the
-- post correspondence problem. it requires recursive data
-- types.

data Foo a b x y = Foo (Bar a b (a x) (b (a (a y))))
                       (Bar a b (a (b x)) (a (a y)))
                       (Bar a b (b (b (a x))) (b (b y)))
 
-- we need duplicate to enforce N>=1
data Bar a b x y = Bar (Bar a b (a x) (b (a (a y))))
                       (Bar a b (a (b x)) (a (a y)))
                       (Bar a b (b (b (a x))) (b (b y)))
 
reduceA :: Bar a b (a x) (a y) -> Bar a b x y
reduceB :: Bar a b (b x) (b y) -> Bar a b x y 

query ? Foo a b c c -> Bar a b c c

Test.hs

-- haskell module to show that in principle, stuff
-- type-checks and there is a solution to the query.

data Foo a b x y = Foo { f1 :: (Bar a b (a x) (b (a (a y))))
                       , f2 :: (Bar a b (a (b x)) (a (a y)))
                       , f3 :: (Bar a b (b (b (a x))) (b (b y)))
                       }
 
-- we need duplicate to enforce N>=1
data Bar a b x y = Bar { b1 :: (Bar a b (a x) (b (a (a y))))
                       , b2 :: (Bar a b (a (b x)) (a (a y)))
                       , b3 :: (Bar a b (b (b (a x))) (b (b y)))
                       }
 
reduceA :: Bar a b (a x) (a y) -> Bar a b x y
reduceA = undefined
reduceB :: Bar a b (b x) (b y) -> Bar a b x y 
reduceB = undefined

query :: Foo a b c c -> Bar a b c c
query = reduceA
      . reduceA
      . reduceB
      . reduceB
      . reduceB
      . reduceA
      . reduceA
      . reduceB
      . reduceB
      . b3 . b2 . b3 . f1