chore: remove Monad List instance

@Kha The new `do` notation works for pure code too.
It automatically inserts `Id` if the expected type is not a monad.
This works great when we are not conflating data and control.
After deleting `Monad List`, we will be able to write functions such as
```lean
def mapWhen (p : Nat → Bool) (f : Nat → Nat) (xs : List Nat) : List Nat := do
for x in xs do
  if p x then
    x := f x
```
without adding `Id.run` before the `do`.

src/Init/Data/List.lean

@@ -6,5 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.List.Basic
 import Init.Data.List.BasicAux
-import Init.Data.List.Instances
 import Init.Data.List.Control

src/Init/Data/List/Instances.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import Init.Data.List.Basic
-import Init.Control.Alternative
-import Init.Control.Monad
-open List
-
-universes u v
-
-instance : Monad List :=
-{ pure := @List.pure, map := @List.map, bind := @List.bind }
-
-instance : Alternative List :=
-{ List.Monad with
-  failure := @List.nil,
-  orelse  := @List.append }

tests/lean/run/bigop.lean

@@ -25,8 +25,8 @@ class Enumerable (α : Type) :=
 instance : Enumerable Bool :=
 { elems := [false, true] }
 
-instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
-{ elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
+-- instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
+-- { elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
 
 partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
 | 0,   h => [⟨0, h⟩]