241 | | '''!!!TODO:''' complete the following. |

242 | | |

243 | | 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: |

244 | | 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`. |

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

246 | | |

247 | | '''!!!TODO:''' What about unflattening the locals? |

248 | | |

249 | | {{{ |

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

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

252 | | }}} |

253 | | |

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

| 242 | 1. '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to all equalities. |

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