How does this trick type-check?

Question

Reading this blog post – https://www.haskellforall.com/2021/05/the-trick-to-avoid-deeply-nested-error.html – I realised I don't understand why the 'trick' actually works in this situation:

{-# LANGUAGE NamedFieldPuns #-}

import Text.Read (readMaybe)

data Person = Person { age :: Int, alive :: Bool } deriving (Show)

example :: String -> String -> Either String Person
example ageString aliveString = do
    age <- case readMaybe ageString of
        Nothing  -> Left "Invalid age string"
        Just age -> pure age

    if age < 0
        then Left "Negative age"
        else pure ()

    alive <- case readMaybe aliveString of
        Nothing    -> Left "Invalid alive string"
        Just alive -> pure alive

    pure Person{ age, alive }

Specifically I'm struggling to understand why this bit

    if age < 0
        then Left "Negative age"
        else pure ()

type checks.

Left "Negative age" has a type of Either String b

while

pure () is of type Either a ()

Why does this work the way it does?

---

EDIT: I simplified and re-wrote the code into bind operations instead of do block, and then saw Will's edit to his already excellent answer:

{-# LANGUAGE NamedFieldPuns #-}

import           Text.Read (readMaybe)

newtype Person = Person { age :: Int} deriving (Show)

example :: String -> Either String Person
example ageString =
    getAge ageString
    >>= (\age -> checkAge age
        >>= (\()-> createPerson age))

getAge :: Read b => String -> Either [Char] b
getAge ageString = case readMaybe ageString of
       Nothing  -> Left "Invalid age string"
       Just age -> pure age

checkAge :: (Ord a, Num a) => a -> Either [Char] ()
checkAge a = if a < 0
       then Left "Negative age"
       else pure ()

createPerson :: Applicative f => Int -> f Person
createPerson a = pure Person { age = a }

I think this makes the 'trick' of passing the () through binds much more visible - the values are taken from an outer scope, while Left indeed short-circuits the processing.

Answer 1

It typechecks because Either String b and Either a () unify successfully, with String ~ a and b ~ ():

     Either String b
     Either a      ()
   ------------------
     Either String ()      a ~ String, b ~ ()

It appears in the do block of type Either String Person, so it's OK, since it's the same monad, Either, with the same "error signal" type, String.

It appears in the middle of the do block, and there's no value "extraction". So it serves as a guard.

It goes like this: if it was Right y, then the do block's translation is

      Right y >>= (\ _ -> .....)

and the computation continues inside ..... with the y value ignored. But if it was Left x, then

      Left x >>= _  =  Left x

according to the definition of >>= for Either. Crucially, the Left x on the right is not the same value as Left x on the left. The one on the left has type Either String (); the one on the right has type Either String Person indeed, as demanded by the return type of the do block overall.

The two Left x are two different values, each with its own specific type. The x :: String is the same, of course.