Changes between Version 89 and Version 90 of TypeFunctionsSolving
 Timestamp:
 Sep 13, 2008 1:58:05 PM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v89 v90 243 243 244 244 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: 245 1. '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''lefthand side''' of all equalities. 246 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`. 245 1. '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to the '''lefthand side''' of all equalities. We also perform the same substitution on all class constraints. 246 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`. (We never instantiate any flexibles introduced by flattening locals.) 247 247 The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check after each substitution. It is an important property of propagation that we only need to substitute into righthand sides during finalisation. 248 249 After finalisation and zonking all flattening of locals is undone (c.f., note below the flattening code above). 248 250 249 251 == Examples ==