В чем разница в выводе типов по сравнению с как-шаблоном в двух аналогичных определениях функций?

Во второй строке left':

left' _ r@(Right _) = r
--      ^^^^^^^^^^^   ^

Поскольку вы используете as-pattern, вам требуется, чтобы тип ввода был равен типу возвращаемого значения, поскольку очевидно, что они имеют одно и то же значение. Тогда тип left' ограничивается чем-то вроде a -> b -> b.

Это ограничение затем распространяется в обратном направлении, чтобы, в свою очередь, ограничить тип функции - надеюсь, вы видите, как это сделать; это не так уж и сложно.

Однако во второй строке left вы создаете новое значение

left _ (Right x) = Right x
--                 ^^^^^^^

Тип этого нового значения не был ограничен, и поэтому та же проблема не возникает; это может быть что-то в форме a -> b -> c, чего вы и хотите.

По этой причине тип left' более ограничен, чем тип left, что является причиной того, что их типы не равны.

Чтобы проиллюстрировать эту концепцию более конкретно, я более точно опишу вам, как это ограничение распространяется в обратном направлении.

Мы знаем, что подпись left' имеет форму (a -> b) -> Either a q -> Either b q. Однако в строке 2 указано Either a q = Either b q, что означает a = b, поэтому тип теперь становится (a -> a) -> Either a q -> Either a q.

Проблема здесь в том, что есть некоторые «скрытые» типы, которые имеют значение. Механизм вывода типов может вывести их в первом случае, но не во втором.

Когда мы используем

Right :: forall a b. b -> Either a b

нам действительно нужно выбрать, какие типы a и b. К счастью, в большинстве случаев этот выбор делает за нас вывод типа. Тип b выбрать легко: это тип значения внутри аргумента Right. Тип a вместо этого может быть чем угодно - машина вывода должна полагаться на контекст, чтобы «заставить» сделать выбор для a. Например, обратите внимание, что все эти типы проверяют:

test0 :: Either Int Bool
test0 = Right True

test1 :: Either String Bool
test1 = Right True

test2 :: Either [(Char, Int)] Bool
test2 = Right True

Теперь в вашей первой функции

left :: (t -> a) -> Either t b -> Either a b
left f (Left x) = Left (f x)
left _ (Right x) = Right x

Первым совпавшим Right x на самом деле является Right x :: Either t b, где в качестве аргументов неявного типа выбраны t и b. Это делает x типом b. Используя эту информацию, вывод типа пытается определить тип для второго Right x. Там он может видеть, что он должен иметь форму Either ?? b, начиная с x :: b, но, как это случилось с нашими test примерами выше, мы можем использовать что угодно для ??. Таким образом, механизм вывода типов выбирает другую переменную типа a (тип, который может быть t, но может быть и другим).

Вместо этого во второй функции

left' :: (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left (f x)
left' _ r@(Right _) = r

мы даем имя (r) шаблону Right _. Как и выше, предполагается, что он имеет тип Either t b. Однако теперь мы используем имя r справа от =, поэтому вывод типа не должен делать здесь никаких выводов и может (фактически, должен) просто повторно использовать тип, для которого он уже определен. r. Это делает тип вывода таким же Either t b, что и тип ввода, и, в свою очередь, заставляет f иметь тип t -> t.

Если это сбивает с толку, вы можете попытаться полностью избежать вывода типов и предоставить явный выбор типов, используя синтаксис Right @T @U для выбора функции U -> Either T U. (Однако для этого вам нужно будет включить расширения ScopedTypeVariables, TypeApplications.) Затем мы можем написать:

left :: forall t a b. (t -> a) -> Either t b -> Either a b
left f (Left x) = Left @a @b (f x)
left _ (Right x) = Right @a @b x
                      -- ^^ -- we don't have to pick @t here!

У нас также может быть

left :: forall t b. (t -> t) -> Either t b -> Either t b
left f (Left x) = Left @t @b (f x)
left _ (Right x) = Right @t @b x

и это будет работать нормально. GHC предпочитает первый тип, поскольку он является более общим, позволяя a быть любым (включая t, но также включая другие типы).

Во втором определении нет приложения типа, которое можно было бы указать, поскольку оно повторно использует то же значение r с правой стороны, что и слева:

left' :: forall t b. (t -> t) -> Either t b -> Either t b
left' f (Left x) = Left @t @b (f x)
left' _ r@(Right x) = r
                   -- ^^ -- can't pick @a here! it's the same as on the LHS