| 1 | == A first (naive) attempt == |

| 2 | |

| 3 | |

| 4 | To solve {{{(C implies t1=t2)}}} with respect to Ax |

| 5 | |

| 6 | 1. We interpret Ax /\ C as a rewrite system (from left to right). |

| 7 | 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. |

| 8 | |

| 9 | |

| 10 | Immediately, we find a problem with this solving strategy. |

| 11 | Consider our running example. |

| 12 | |

| 13 | Rewrite rules |

| 14 | {{{ |

| 15 | (forall a. S [a] = [S a]) /\ (R1) -- axioms |

| 16 | (T Int = Int) (R2) |

| 17 | |

| 18 | /\ |

| 19 | |

| 20 | (T [Int] = S [Int]) /\ (R3) -- local assumptions |

| 21 | (T Int = S Int) (R4) |

| 22 | }}} |

| 23 | |

| 24 | applied to {{{(T [Int] = [Int])}}} |

| 25 | |

| 26 | yields |

| 27 | {{{ |

| 28 | T [Int] -->* [S Int] (R3,R1) |

| 29 | |

| 30 | [Int] -->* [Int] |

| 31 | }}} |

| 32 | |

| 33 | Hence, our (naive) solver fails, but |

| 34 | clearly the (local) property (T [Int] = [Int]) |

| 35 | holds. |

| 36 | |

| 37 | The trouble here is that |

| 38 | |

| 39 | * the axiom system Ax is confluent, but |

| 40 | * if we include the local assumptions C, the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) |

| 41 | |

| 42 | |

| 43 | Possible solutions: |

| 44 | |

| 45 | Enforce syntactic conditions such that Ax /\ C is confluent. |

| 46 | It's pretty straightforward to enforce that Ax and |

| 47 | constraints appearing in type annotations and data types |

| 48 | are confluent. The tricky point is that if we combine |

| 49 | these constraints they may become non-confluent. |

| 50 | For example, imagine |

| 51 | |

| 52 | {{{ |

| 53 | Ax : T Int = Int |

| 54 | |

| 55 | a= T Int -- from f :: a=T Int => ... |

| 56 | |

| 57 | implies |

| 58 | |

| 59 | (a = S Int -- from a GADT pattern |

| 60 | |

| 61 | implies ...) |

| 62 | }}} |

| 63 | |

| 64 | The point is that only during type checking we may |

| 65 | encounter that Ax /\ C is non-confluent! |

| 66 | So, we clearly need a better type checking method. |

| 67 | |

| 68 | |