453 | | * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family in `t` must be strictly less than the number of data type constructor and variable symbols in `s`. |
454 | | |
455 | | We require that all axioms and local assumptions are normal. In particular, all type family instances and all equalities in signatures need to be normal. NB: With `-fundecidable-indexed-types`, we can drop left linearity and decreasingness. |
| 455 | * ''Decreasing'': The number of data type constructor and variables symbols occurring in the arguments of a type family occuring in `t` must be strictly less than the number of data type constructor and variable symbols in `s`. |
| 456 | |
| 457 | Examples of normal type equations: |
| 458 | {{{ |
| 459 | data C |
| 460 | type instance Id a = a |
| 461 | type instance F [a] = a |
| 462 | type instance F (C (C a)) = F (C a) |
| 463 | type instance F (C (C a)) = F (C (Id a)) |
| 464 | type instance F (C (C a)) = C (F (C a)) |
| 465 | type instance F (C (C a)) = (F (C a), F (C a)) |
| 466 | }}} |
| 467 | |
| 468 | Examples of type equations that are ''not'' normal: |
| 469 | {{{ |
| 470 | type instance F [a] = F (Maybe a) -- Not decreasing |
| 471 | type instance G a a = a -- Not left linear |
| 472 | type instance F (G a) = a -- Not constructor-based |
| 473 | type instance F (C (C a)) = F (C (Id (C a))) -- Not decreasing |
| 474 | }}} |
| 475 | Note that `forall a. (G a a = a) => a -> a` is fine, as `a` is a rigid variables, not a schema variable. |
| 476 | |
| 477 | We require that all type family instances are normal. Moreover, all equalities arising as local assumptions need to be such that they can be normalised (see below). NB: With `-fundecidable-indexed-types`, we can drop left linearity and decreasingness. |
| 478 | |
| 479 | === Normalisation of equalities === |
| 480 | |
| 481 | Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` leads to a (possibly empty) set of normal equations, or to a type error. We proceed as follows: |
| 482 | |
| 483 | 1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`. |
| 484 | 2. If `s'` and `t'` are the same variable, we succeed (with no new rule). |
| 485 | 3. If `s'` and `t'` are distinct rigid variables, we fail. |
| 486 | 4. If `s'` or `t'` is a wobbly type variables, instantiate it with the other type (after occurs check). |
| 487 | 5. If `s'` = `C1 ...` and `t' = C2 ...`, where `C1` and `C2` are different data type constructors, we reject the program. |
| 488 | 6. If `s'` = `C s1 .. sn` and `t'` = `C t1 .. tn`, then yield the union of the equations obtained by normalising all `ti = si`. |
| 489 | |
| 490 | Rejection of local assumptions that after normalisation are either not left linear or not decreasing may lead to incompleteness. However, this should only happen for programs that combine GADTs and type functions in ellaborate ways. |