Можно ли отменить обходы по типу?

Ваша установка надежна, и IxBackwards является полезной (на самом деле, критической) - проблема, с которой вы столкнулись, заключается в том, что обе переменные Dual и Reverse меняют местами переменные типа, тогда как первый аргумент ttraverse требует позиции переменных квантифицированного типа (x,y), чтобы «согласовываться» в некотором смысле. Вы должны одновременно «перевернуть» эти переменные в рекурсивном вызове ttraverse, используя оба Dual и IxBackwards:

instance TTraversable t => TTraversable (Reverse t) where

  ttraverse f = 
    ixmap Reverse . ixforwards . 
    ttraverse (IxBackwards . ixmap Dual . f . getDual) . 
    unReverse 

Написание экземпляров для TFunctor и TFoldable может дать подсказку, как найти эту реализацию:

dualNat2 :: (c ~~> d) -> Dual c ~~> Dual d 
dualNat2 k (Dual x) = Dual $ k x 

instance TFunctor f => TFunctor (Reverse f) where 
  tmap f (Reverse q) = Reverse $ tmap (dualNat2 f) q 

instance TFoldable f => TFoldable (Reverse f) where 
  tfoldMap k (Reverse z) = getDual $ tfoldMap (dualNat2 k) z 

По сути, вы делаете то же самое в случае TTraversable, за исключением того, что теперь нужно перевернуть два индекса:

f                                      :: forall x y . c x y -> f x y (d x y)   
ixmap Dual . f . getDual               :: forall x y . Dual c y x -> f x y (Dual d y x)
IxBackwards . f                        :: forall x y . c x y -> IxBackwards f y x (d x y)
IxBackwards . ixmap Dual . f . getDual :: forall x y . Dual c y x -> IxBackwards f y x (Dual d y x)

и обратите внимание, что если вы перевернете только один из индексов, тип функции даже не будет соответствовать типу аргумента ttraverse.

Я попытаюсь дать пошаговый вывод, используя Typed Holes.

Начните с этого скелета, который, как мне кажется, легко вывести:

  ttraverse f = 
    ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

Это дает ошибку типа:

Couldn't match type `q' with `p'
...
Expected type: Reverse t c p q -> f p q (Reverse t d p q)
Actual type: Reverse t c q p -> f p q (Reverse t d q p)
* In the expression: ixmap Reverse . ttraverse _trfun . unReverse

Так что добавляйте больше отверстий, пока он не скомпилируется. Мой первый порыв — добавить еще одну дыру впереди (поскольку ошибка типа относится ко всему выражению, нужно что-то сделать со всем выражением, чтобы проверить тип):

  ttraverse f = 
    _out . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

Теперь мы не получаем ошибок типа (игнорируя ошибки «двусмысленного типа» в форме C x, где C — класс — есть ошибочные), а сообщаемый тип —

 _out :: f0 q p (Reverse t c0 p q) -> f p q (Reverse t d p q)

где f0, c0 - это (в настоящее время) переменные свободного типа, которые мы используем в наших интересах! Если мы допустим c0 ~ d и f0 ~ IxBackwards f, то это как раз тип ixforwards — так что попробуем:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse _trfun . 
    unReverse 

и теперь мы получаем хороший мономорфный выводимый тип:

 _trfun :: Dual c x y -> IxBackwards f x y (Dual d x y)
 * Relevant bindings include
     f :: forall (x :: r) (y :: r). c x y -> f x y (d x y)

Теперь я также предполагаю, что очевидно, что _trfun каким-то образом должен использовать f, так что давайте попробуем. Мы замечаем, что и домен, и диапазон f не совсем совпадают с _trfun, поэтому мы размещаем отверстия с обеих сторон:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . f . _in) . 
    unReverse 

и получить:

_out :: f x0 y0 (d x0 y0) -> IxBackwards f x y (Dual d x y)
_in :: Dual c x y -> c x0 y0

где x0, y0 — свободные переменные. Вероятно, наиболее очевидно, что с x0 ~ y, y0 ~ x у нас есть _in = getDual, поэтому мы пробуем это и получаем новый предполагаемый тип:

_out :: f y x (d y x) -> IxBackwards f x y (Dual d x y)

и теперь очевидно, что переменные типа «перевернуты» в двух разных местах; один раз IxBackwards и один раз Dual. Способ перевернуть первую пару индексов наиболее очевиден (вероятно):

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (_out . IxBackwards . f . getDual) . 
    unReverse 

и получить:

_out :: IxBackwards f x y (d y x) -> IxBackwards f x y (Dual d x y)

Теперь у нас есть что-то вида q A -> q B с IxFunctor q, поэтому установив _out = ixmap _out получаем

_out :: d y x -> Dual d x y

и есть тривиальная функция этого типа, а именно Dual, которая завершает определение:

  ttraverse f = 
    ixforwards . ixmap Reverse .  
    ttraverse (ixmap Dual . IxBackwards . f . getDual) . 
    unReverse 

Обратите внимание, как некоторые композиции функций перевернуты по сравнению с исходной версией — я притворился, что не знаю ответа априори, и получил его «наиболее очевидным» способом, заполнив элементы, которые сначала самый простой. Эти два определения эквивалентны (действительно эквивалентны, так как Dual и IxBackwards оба просто newtypes).