Changes between Version 99 and Version 100 of TypeFunctionsSolving
- Apr 14, 2009 7:39:02 AM (5 years ago)
v99 v100 248 248 249 249 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). We perform finalisation in two phases: 250 1. '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''right-hand side''' of all equalities. We also perform the same substitution on class constraints. 250 1. '''Substitution:''' 251 * '''Pass A:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''right-hand side''' of all equalities. We also perform the same substitution on class constraints. 252 * '''Pass B:''' For any family equality of the form `co :: F t1..tn ~ alpha`, we apply the substitution `[F t1..tn/alpha]` to the '''both sides''' of all family equalities. 251 253 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`. Moreover, we have to do the same for equalities of the form `co :: F t1..tn ~ alpha` unless we are in inference mode and `alpha` appears in the environment or any other wanteds. (We never instantiate any flexibles introduced by flattening locals.) 252 254 The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. We need to instantiate all flexibles that arose as skolems during flattening of wanteds ''before'' we instantiate any other flexibles. Consider `F delta ~ alpha, F alpha ~ delta`, where `alpha` is a skolem and `delta` a free flexible. We need to produce `F (F delta) ~ delta` (and not `F (F alpha) ~ alpha`). Otherwise, we may wrongly claim to having performed an improvement, which can lead to non-termination of the combined class-family solver.