| 255 | |

| 256 | == Examples == |

| 257 | |

| 258 | === Unflattening locals and finalisation === |

| 259 | |

| 260 | This seems ok: |

| 261 | {{{ |

| 262 | c :: a ~ [F b] |- gamma :: alpha ~ a |

| 263 | =(norm)=> |

| 264 | c :: a ~ [beta], id :: F b ~ beta |- gamma :: alpha ~ a |

| 265 | =(final)=> |

| 266 | alpha := a, gamma := id |

| 267 | }}} |

| 268 | |

| 269 | The problem becomes obvious when we orient the wanted equality the other way around: |

| 270 | {{{ |

| 271 | c :: a ~ [F b] |- gamma :: a ~ alpha |

| 272 | =(norm)=> |

| 273 | c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha |

| 274 | =(SubstVarVar)=> |

| 275 | c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha |

| 276 | with gamma := c |> gamma' |

| 277 | =(norm)=> |

| 278 | c :: a ~ [beta], id :: F b ~ beta |- gamma'' :: alpha ~ [beta] |

| 279 | with gamma' := sym gamma'' |

| 280 | =(final)=> |

| 281 | alpha := [beta], gamma'' := id |

| 282 | }}} |

| 283 | What about `F b ~ beta`? If we just throw that away, we have an unconstrained `beta` in the environment. However, instantiating `beta` with `F b` doesn't seem to be right, too (considering Andrew Kennedy). |

| 284 | |

| 285 | Let's assume one toplevel equality `forall x. g x :: F x = ()`: |

| 286 | {{{ |

| 287 | c :: a ~ [F b] |- gamma :: a ~ alpha |

| 288 | =(norm)=> |

| 289 | c :: a ~ [beta], id :: F b ~ beta |- gamma :: a ~ alpha |

| 290 | =(SubstVarVar)=> |

| 291 | c :: a ~ [beta], id :: F b ~ beta |- gamma' :: [beta] ~ alpha |

| 292 | with gamma := c |> gamma' |

| 293 | =(norm)=> |

| 294 | c :: a ~ [beta], id :: F b ~ beta |- gamma'' :: alpha ~ [beta] |

| 295 | with gamma' := sym gamma'' |

| 296 | =(Top)=> |

| 297 | c :: a ~ [beta], sym (g b) :: () ~ beta |- gamma'' :: alpha ~ [beta] |

| 298 | =(norm)=> |

| 299 | c :: a ~ [beta], g b :: beta ~ () |- gamma'' :: alpha ~ [beta] |

| 300 | =(final)=> |

| 301 | alpha := [beta], gamma'' := id |

| 302 | }}} |

| 303 | This is obviously bad, as we want to get `alpha := [()]` and not `alpha := [beta]` for a free `beta` out of finalisation. |

| 304 | |