| 433 | |

| 434 | ---- |

| 435 | |

| 436 | == Restrictions on valid programs == |

| 437 | |

| 438 | We impose some syntactic restrictions on programs to ensure that type checking remains (a) deterministic, (b) a simple rewrite model is sufficient to reduce type function applications, and (c) it hopefully remains decidable. |

| 439 | |

| 440 | === Type variables === |

| 441 | |

| 442 | We have three kinds of type variables: |

| 443 | |

| 444 | * ''Schema variables'' |

| 445 | |

| 446 | === Normal type equations === |

| 447 | |

| 448 | ''Normal type equations'' `s = t` obey the following constraints: |

| 449 | |

| 450 | * ''Constructor based'': The left-hand side `s` must have for form `F s1 .. sn` where `F` is a type family and no type family occur in the `si`. |

| 451 | * ''Non-overlapping'': For any other axiom or local assumption `s' = t'`, there may not be any substitution ''theta'', such that (''theta'' `s`) equals (''theta'' `s'`). |

| 452 | * ''Left linear'': No schema variable appears more than once in `s`. |

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