Aiding Dependent Type Checking with Rewrite Rules (2007)
Dependent type checking in Cayenne often fails when the programmer has relied on non-trivial properties of functions that are used in types. For instance, associativity of addition on natural numbers...