We interpret Ax /\ C as a rewrite system (from left to right).
We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent.
Immediately, we find a problem with this solving strategy.
Consider our running example.
(forall a. S [a] = [S a]) /\ (R1) -- axioms(T Int = Int) (R2) /\(T [Int] = S [Int]) /\ (R3) -- local assumptions(T Int = S Int) (R4)
applied to (T [Int] = [Int])
T [Int] -->* [S Int] (R3,R1)[Int] -->* [Int]
Hence, our (naive) solver fails, but
clearly the (local) property (T [Int] = [Int])
The trouble here is that
the axiom system Ax is confluent, but
if we include the local assumptions C, the combined system Ax /\ C is non-confluent (interpreted as a rewrite system)
Enforce syntactic conditions such that Ax /\ C is confluent.
It's pretty straightforward to enforce that Ax and
constraints appearing in type annotations and data types
are confluent. The tricky point is that if we combine
these constraints they may become non-confluent.
For example, imagine
Ax : T Int = Int a= T Int -- from f :: a=T Int => ... implies (a = S Int -- from a GADT pattern implies ...)
The point is that only during type checking we may
encounter that Ax /\ C is non-confluent!
So, we clearly need a better type checking method.