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 (----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.