I fully agree with Iavor. The correctness criterion is the declaration class C a b | a -> b implies that the following implication must hold: C a1 b1, C a2 b2, a1 ~ a1 ===> b1 ~ b2 That implication lets us derive the proof of type equality, which we can use for improving other types and resolving further constraints. Here is a little Prolog program that helps us decide which instance declarations should be accepted, and which are in error (regardless of the Undecidable instances flag). The program currently works when there is no overlapping. The program is a simple model checker for the above implication. Ex1: % class C a b | a -> b % instance C Int Bool % instance C a b c(int,bool). c(_A,_B). ?- c(X,Y), c(X,Y1), disunify(Y,Y1), print(['counterexample: ', c(X,Y), c(X,Y1)]). %% [counterexample: , c(int, bool), c(int, e7)] A counter-example was found. The instances must be rejected. Ex2:
Wait. What about instance C [a] [b]
% class C a b | a -> b % instance C Int Bool % instance C [a] [b] c(int,bool). c([_A],[_B]). ?- c(X,Y), c(X,Y1), disunify(Y,Y1), print(['counterexample: ', c(X,Y), c(X,Y1)]). %% [counterexample: , c([_G2442], [e8]), c([_G2442], [e9])] Reject. Ex3: % class C a b | a -> b % instance C Int Bool % instance C [a] a c(int,bool). c([_A],_A). ?- c(X,Y), c(X,Y1), disunify(Y,Y1), print(['counterexample: ', c(X,Y), c(X,Y1)]). %% No counter-examples. Accept. Ex4:
What about the following code--do you think this should be illegal, too? class C a b c | a -> b where instance C (Maybe a) (Maybe b) (Maybe b) where
c(maybe(_A),maybe(_B),maybe(_B)). ?- c(X,Y,Z), c(X,Y1,Z1), disunify(Y,Y1), print(['counterexample: ', c(X,Y,Z), c(X,Y1,Z1)]). %% [counterexample: , c(maybe(_G2446), maybe(e11), maybe(e11)), %% c(maybe(_G2446), maybe(e12), maybe(e12))] Illegal. Ex5:
But now you are going to end up rejecting programs like this: class C a b | a -> b class D a b | a -> b instance (D a b) => C [a] [b]
d(int,bool). % Need an instance for D; otherwise, we won't type check. c([A],[B]) :- d(A,B). ?- c(X,Y), c(X,Y1), disunify(Y,Y1), print(['counterexample: ', c(X,Y), c(X,Y1)]). %% Failed, no counter-examples. Accepted. Ex6: %% class C a a' b | a a' -> b %% class D a b | a -> b %% instance (D a b) => C [a] [a'] [b] d(int,bool). % Need an instance for D; otherwise, we won't type check. c([A],[A1],[B]) :- d(A,B). ?- c(X,Y,Z), c(X1,Y1,Z1), [X,Y] = [X1,Y1], disunify(Z,Z1), print(['counterexample: ', c(X,Y,Z), c(X1,Y1,Z1)]). %% Failed to find a counter-example. Accept. Here is the definition of disunify. eigen(X) :- gensym(e,X). % Ground a term, instantiating all of its variables to fresh constants instantiate(T) :- term_variables(T,Vars), maplist(eigen,Vars). % disunify(T1,T2) % Holds if T1 and T2 are not unifiable, or can be made non-unifiable. % If succeeds, T1 and T2 are ground and T1 \= T2. disunify(T1,T2) :- instantiate(T1), copy_term(T2,T21), (T1 = T21 -> instantiate(T2), \+ (T1=T2); true).