| 100 | "Derived" constraints are facts that are implied by the constraints |

| 101 | in the inert set. They do not have complete proofs because their |

| 102 | proof may depend on proofs of as yet unsolved "wanted" constraints. |

| 103 | GHC does not associate any proof terms with "derived" constraints. |

| 104 | In the constraint solver, they are mostly used as "hints". For example, |

| 105 | consider the wanted constraint {{{5 + 3 ~ x}}}, where {{{x}}} is a |

| 106 | free unification variable. These are the steps we'll take to solve |

| 107 | the constraint: |

| 108 | |

| 109 | {{{ |

| 110 | Rules: |

| 111 | Add_def(5,3) : 5 + 3 ~ 8 |

| 112 | Add_fun : forall a b c1 c2. (a + b ~ c1, a + b ~ c2) => c1 ~ c2 |

| 113 | |

| 114 | 1. Add [W] C: 5 + 3 ~ x to inert set |

| 115 | 2. Generate new derived: |

| 116 | [D] Add_fun(C,Add_def) : x ~ 8 (proof discarded) |

| 117 | 3. GHC uses this hint to improve the wanted to [W] C: 5 + 3 ~ 8 |

| 118 | 4. Solved: |

| 119 | [W] C = Add_def(5,3) |

| 120 | }}} |

| 121 | |

| 122 | |

| 123 | |

| 124 | |

| 125 | |

| 126 | |

| 127 | |

| 128 | |

| 129 | |

| 130 | |

| 131 | |

| 132 | |

| 133 | |

| 134 | |

| 135 | |

| 136 | |