| 90 | Eg: G Int ~ Bool |

| 91 | }}} |

| 92 | Completion gives: |

| 93 | {{{ |

| 94 | Eg |

| 95 | => (TOP) |

| 96 | VOID ~ Bool |

| 97 | => FAIL |

| 98 | }}} |

| 99 | |

| 100 | We can be a bit more tricky and use |

| 101 | {{{ |

| 102 | Et: {F [a] ~ F (G a); F _ ~ VOID} |

| 103 | {G _ ~ VOID} |

| 104 | |

| 105 | Eg: G x ~ [x] |

| 106 | }}} |

| 107 | Here the idea is to use a new symbol in the local given, namely a rigid type variable. Nevertheless, the only equality of `G` matches `G x` and completion of `Eg` leads to an inconsistency. |

| 108 | |

| 109 | However, if we add another equality to `G`, the situation changes: |

| 110 | {{{ |

| 111 | Et: {F [a] ~ F (G a); F _ ~ VOID} |

| 112 | {G Int ~ Bool; G _ ~ VOID} |

| 113 | |

| 114 | Eg: G x ~ [x] |

| 115 | }}} |

| 116 | Here completion can't rewrite `G x`, as the outcome depends on getting more information about `x`. However, we have the following infinite derivation: |

| 117 | {{{ |

| 118 | F [x] --> F (G x) --> F [x] --> ... |

| 119 | }}} |

| 120 | This is although `Eg` is inconsistent (and hence shouldn't be used for rewriting at all). |

| 121 | |

| 122 | Can we fix this??? |