Update TypeDD Chapter 11 for idris2

[trevarj]

There is a difference between idris1 and idris2 which breaks backwards compatibility when trying to implement (>>=) to use do notation for a custom type. See #1095 for details.

[trevarj]

Can someone help clarify this sentence to make it more accurate?

When implementing (>>=) to support do notation for custom types, like RunIO, you must now add an extra data constructor (>>) to help desugaring.

[stefan-hoeck]

How about:

In order to support do notation for custom types, you need to implement (>>=) for binding values in a do block and (>>) for sequencing computations without binding values.
For instance, the following do block is desugared to foo >>= (\x => bar >>= (\y => baz x y)):

do
  x <- foo
  y <- bar
  baz x y

while the following is converted to foo >> bar >> baz:

do
  foo
  bar
  baz

[trevarj]

@stefan-hoeck this is perfect, thanks! Helps me immediately understand what the reason for adding the data constructor and >> is.

[mattpolzin]

Great addition to the book notes. Thanks!

[gallais]

Thank you for the patch! Sorry I didn't think to fix the notes when I saw the typedd tests were failing. 😞

[trevarj]

@gallais Not a problem. Happy to help and learn!