The infinite loop case is:

    loopType : Int -> Type
    loopType x = loopType x

    foo : List (loopType 3) -> Int
    foo _ = 42

    bar : List (loopType 4)
    bar = []

    baz : Int
    baz = foo bar

Determining if baz type-checks requires evaluating loopType 3 and loopType 4 to determine if they're equal.