234 | | If only flexible type equalities remain as wanted equalities, the locals entail the wanteds. We can now instantiate type variables in flexible type equalities where possible to propagate constraints into the environment. In GHC, we may wrap any remaining equalities (of any form) into an implication constraint to be propagated outwards (where it may be solved under an extended set of local equalities.) |

235 | | |

236 | | Notes: |

237 | | |

238 | | * (Unify) is an asymmetric rule, and hence, only fires for equalities of the form `x ~ c`, where `c` is free of synonym families. Moreover, it only applies to wanted equalities. (Rationale: Local equality constraints don't justify global instantiation of flexible type variables - just as in new-single.) |

| 234 | The finalisation step instantiates as many flexible type variables as possible, but it takes care to not to affect variables occurring in the global environment. The latter is important to obtain principle types (c.f., Andrew Kennedy's thesis). Hence, we perform finalisation in two phases: |

| 235 | 1. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted or `alpha` is a variable introduced by flattening, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. |

| 236 | 2. '''Substitution:''' For any family equality... |

| 237 | |

| 238 | {{{ |

| 239 | alpha in environ, beta in skolems: |

| 240 | gamma1 :: alpha ~ [beta], id :: G a ~ beta -- , gamma2 :: F a ~ beta |

| 241 | }}} |