Update phantom-types.md

Some edits to make the content clear! 

Good!

Author: biboudis

docs/docs/reference/phantom-types.md

@@ -7,25 +7,21 @@ title: "Phantom Types"
 What is a phantom type?
 -----------------------
 
-A phantom type is a manifestation of abstract type that has no effect on the runtime. 
-These are useful to prove static properties of the code using type evidences. 
-As they have no effect on the runtime they can be erased from the resulting code by 
-the compiler once it has shown the constraints hold.
-
-When saying that a they have no effect on the runtime we do not only mean side effects 
-like IO, field mutation, exceptions and so on. We also imply that if a function receives 
-a phantom its result will not be affected by this argument.
-
-As phantom do not live at runtime they cannot be subtypes of `scala.Any`, which deffines 
-methods such as `hashCode`, `equals`, `getClass`, `asInstanceOf` and `isInstanceOf`. 
-All these operations cannot exist on phantoms as there will not be an underlying object 
-instance at runtime. At first glace this could look like a limitation, but in fact not 
-having `asInstanceOf` will make constraints more reliable as it will not be possible to 
-downcast a phantom value to fake an evidence.
-
-If they don't live in the universe bounded by `scala.Any` and `scala.Nothing` where do 
-they live? The answer is in their own type universes bounded by their phantom `Any` and `Nothing`. 
+A phantom type is a manifestation of an abstract type that has no effect on the runtime execution of the program. 
+Phantom types are useful to prove static properties of the code, using evidence or witnesses that the aforementioned properties hold at the type level.
+The most significant property of phantom types is that they have no _effect_ on the runtime since they can be erased from the resulting code by the compiler once it has shown that the constraints hold.
+
+When saying that they have no effect on the runtime we not only mean side effects 
+such as IO, field mutation, exceptions but also that the result of a function receiving a phantom will not be affected by this argument.
+
+Phantoms are not represented by an object instance at runtime.
+Subsequently, since phantoms do not live at runtime, they cannot be subtypes of `scala.Any`, which defines methods such as `hashCode`, `equals`, `getClass`, `asInstanceOf` and `isInstanceOf`. 
+At first glace this could look like a limitation.
+However, by not having `asInstanceOf` makes constraints more reliable as it will not be possible to downcast a phantom value to fake an evidence.
+
+An interesting question is the following: if they don't live in the _type universe_, bounded by `scala.Any` and `scala.Nothing`, where do they live? The answer is in their own type universes bounded by their phantom `Any` and `Nothing`. 
 In fact we allow multiple phantom universes to exist.
+In the following figure we demonstrate three such universes.
 
 ```none
           +-----+                     +---------------+           +--------------------+
@@ -49,15 +45,16 @@ In fact we allow multiple phantom universes to exist.
          +---------+                +-------------------+       +------------------------+
 ```
 
-Inside a universe it types support the full Dotty type system. But we cannot mix types from 
-different universes with `&`, `|` or in type bounds. Each type must be fully defined one universe.
-
+Inside a universe types support the full Dotty type system. 
+However, we cannot mix types from different universes with `&`, `|` or in type bounds. 
+Each type must be fully defined one universe.
 
 Implement your own phantom type
 -------------------------------
 Phantom types are definded by an `object` extending `scala.Phantom`. This object will represent 
 a universe of phantom types that is completely separated from types in `scala.Any` or other 
-phantom universes. We can define our phantom universe `MyPhantoms`.
+phantom universes. 
+Let us define our phantom universe `MyPhantoms` for exposition:
 
 ```scala
 object MyPhantoms extends Phantom
@@ -74,15 +71,15 @@ trait Phantom { // only an `object` can extend this trait
 
 The types in the phantom universe are defined by the top type `Phantom.Any` and bottom type 
 `Phantom.Nothing`. This means that `MyPhantoms.Any` and `MyPhantoms.Nothing` are the bounds 
-of the phantom types in `MyPhantoms`, these bounds are `protected` and can not be accessed 
+of the phantom types in `MyPhantoms`. These bounds are `protected` and can not be accessed 
 from outside `MyPhantoms` unless an alias is defined for them.
 
 New phantom types can be defined using `type XYZ <: OtherPhantom` (where `>: MyPhantom.Nothing` 
-will be inferred), this would be the equivalent of `class XYZ extends OtherClass` on a types 
-only (no runtime definitions). Or aliased with `type MyAny = OtherPhantom`. Whitin `MyPhantoms` 
-it is possible to refer to `MyPhantoms.Any` and `MyPhantoms.Nothing` with `this.Any` and 
-`this.Nothing` (or just `Any` and `Nothing` but not recommended). Using this we will define 
-four the four phantoms: `Inky`, `Blinky`, `Pinky` and `Clyde`.
+will be inferred). This would be the equivalent of `class XYZ extends OtherClass` on types 
+only (no runtime definitions). Additionally, phantom types can be aliased with `type MyAny = OtherPhantom`. 
+Within `MyPhantoms` it is possible to refer to `MyPhantoms.Any` and `MyPhantoms.Nothing` with `this.Any` and 
+`this.Nothing` (or just `Any` and `Nothing`, although not recommended). 
+Using this we will define the following four phantoms: `Inky`, `Blinky`, `Pinky` and `Clyde`.
 
 ```scala
 object MyPhantoms extends Phantom {
@@ -93,10 +90,10 @@ object MyPhantoms extends Phantom {
 }
 ```
 
-Values of phantom type can be created using the `protected def assume`. This value can be 
-used as a value of this phantom type as it's type is `this.Nothig` (or `MyPhantoms.Nothing`). 
-Usually this value will be used to define a `implicit def` that returns the phantom with a more 
-precise type. In our example we will only create values of type `Pinky` and `Clyde`
+Values of phantom types can be created using the `protected def assume`. This value can be 
+used as the value of a phantom type since its bottom type is `this.Nothing` (or `MyPhantoms.Nothing`). 
+Usually this value will be used to define an `implicit def` that returns a phantom with a more 
+precise type. In our example we will only create values of type `Pinky` and `Clyde`:
 
 ```scala
 object MyPhantoms extends Phantom {
@@ -109,7 +106,7 @@ object MyPhantoms extends Phantom {
 
 ### Using the phantoms
 
-From the user of the phantom type there is almost no difference, except for stronger type guarantees. 
+From the user's perspective, the difference between a type and a phantom type is that the latter is used when we need stronger type guarantees. 
 We can look at the following simple application:
 
 ```scala
@@ -123,23 +120,23 @@ object MyApp {
 }
 ```
 
-Note given the way we defined the phantoms it is impossible to call the `hide` as we did not 
-expose any value of type `Blinky` to the user. We cannot call `hide(MyPhantoms.assume)` as 
-`assume` is protected, `hide(null.asInstanceOf[Blinky])` does not compile because it is impossible 
-to cast to a phantom and `hide(throw new Exception)` (or `hide(???)`) does not compile as `throw` of
-type `scala.Nothing` is not in the same type universe as `Blinky`. Good, we caught all possible 
-mistakes before when compiling the code, no surprises at runtime (hopefully not in production).
+Note that given the way we defined the phantoms it is impossible to call the `hide` as we did not 
+expose any value of type `Blinky` to the user. On the contrary, we cannot call `hide(MyPhantoms.assume)` as 
+`assume` is protected and `hide(null.asInstanceOf[Blinky])` does not compile because it is impossible 
+to cast to a phantom. `hide(throw new Exception)` (or `hide(???)`) does not compile as `throw` of
+type `scala.Nothing` is not in the same type universe as `Blinky`. 
+Good, we caught all possible mistakes before when compiling the code, no surprises at runtime (hopefully not in production).
 
 
 What happens with Phantoms at runtime?
 --------------------------------------
 
 Disclaimer: Most of phantom erasure is implemented, but not all of is has been merged in `dotty/master` yet.
 
-As phantom have no effect on the result of a method invocation we just remove them for the call an definition. 
-The evaluation of the phantom parameter is still be done unless it can be optimized away. 
-By removing them we also restrict overloading as `def f()` and `def f(x: MyPhantom)` will 
-have the same signature in the bytecode, just use different names to avoid this.
+As phantoms have no effect on the result of a method invocation we just remove them from the actual call. 
+The evaluation of the phantom parameter is still being done unless it can be optimized away. 
+By removing them we also restrict overloading.
+`def f()` and `def f(x: MyPhantom)` will have the same signature in the bytecode, just use different names to avoid this.
 
 At runtime the `scala.Phantom` trait will not exist.
 * The object extending `Phantom` will not extend it anymore
@@ -159,7 +156,7 @@ object MyOtherPhantom extends Phantom {
 }
 ```
 
-will be compiled to
+will be compiled to:
 
 ```scala
 object MyOtherPhantom {