The code is a bit of a gimmick, not really the sort of thing you'd have in a real program. It's just there to demonstrate that the compiler doesn't need explicitly telling which typeclasses associated types correspond to. That said:

    fn show_negative A : A -> Str where
        A < Neg,
        A.Output < Neg,
        A.Output.Output < Neg,
        A.Output.Output.Output < Neg,
        A.Output.Output.Output.Output < Show,
    =
        a => (----a)->show

This is a function, called `show_negative`, that is generic over a type, `A`. The function takes an instance of `A` and returns a `Str` (string).

In terms of implementation, the function is quite simple: it just negates the input value a bunch of time and then `show`s it as a string using the `Show` typeclass (equivalent to Haskell's `show`: https://hackage.haskell.org/package/base-4.16.1.0/docs/Prelu...).

Arithmetic operations such as negation are defined using typeclasses. Here's the definition of `Neg`:

    class Neg =
        => Output
        => neg : Self -> Self.Output

This means that types that can be negated must provide two things: an output type produced when they're negated, and a function that actually performs the negation. For example, `Nat` (natural number) looks like:

    member Nat of Neg =
        => Output = Int
        => neg = fn x => (implementation omitted because it's a built-in intrinsic)

i.e: when you negate a `Nat`, you get an `Int`.

The `where` clauses on the `show_negative` just constrains the output type of negating the `A` in such a way that its output type is also constrained, in a chain, with the final type in the chain being `show`-able.