Add lawful subclasses of existing type classes

[jespercockx]

It would be good to have standard definitions of the type class laws for the classes in the Prelude, and prove them for the instances we provide. Here is an example of how this would look:

open import Haskell.Prelude

record LawfulMonad (m : Set → Set) {{iMonad : Monad m}} : Set₁ where
  field
    left-id  : ∀ {a b} (x : a) (f : a → m b)
             → (return x >>= f) ≡ f x
    right-id : ∀ {a} (k : m a)
             → (k >>= return) ≡ k
    assoc    : ∀ {a b c} (k : m a) (f : a → m b) (g : b → m c)
             → ((k >>= f) >>= g) ≡ (k >>= (λ x → f x >>= g))
open LawfulMonad

instance
  _ : LawfulMonad Maybe
  _ = λ where
    .left-id → λ x f → refl
    .right-id Nothing → refl
    .right-id (Just x) → refl
    .assoc Nothing f g → refl
    .assoc (Just x) f g → refl

Classes for which we should define laws:

• [x] Eq and Ord
• [x] Num
• [ ] BoundedBelow, BoundedAbove, and Bounded
• [ ] Enum
• [x] Semigroup and Monoid
• [x] Functor, Applicative, and Monad
• [ ] Foldable and Traversable

[pmbittner]

As part of PR #331, I implemented the Laws and instances for the Num typeclass. Sorry for spamming the issue feed on accident here with all my rebases. I will take better care with my commit messages / rebases in the future.