To make it legal: If foo' with a type signature doesn't type check, try to infer a type without a signature. If this succeeds then check that the type that was inferred is alpha-convertible to the original signature. If it is, accept foo'; the signature doesn't add any information.
This harder, if not impossible. What does it mean for two signatures to be "alpha-convertible"?
..[type synonym expansion vs type synonym family reduction]
So, I guess, you don't really mean alpha-convertible in its original syntactic sense. We should accept the definition if the inferred and the given signature are in some sense "equivalent". For this "equivalence" to be robust, I am sure we need to define it as follows, where <= is standard type subsumption:
t1 "equivalent" t2 iff t1 <= t2 and t2 <= t1
i would like to express my doubts about this assumption (which relates directly to the earlier discussion about subsumption). no matter what subsumption or what semantic equivalence we are talking about, we expect it to *include* syntactic identity (reflexivity of the relations): forall t: t <= t forall t: t ~ t moving some equational theory into the "syntactic" equivalence does not imply that syntactic has to be the full semantic equivalence - as the example of alpha- vs beta+alpha- convertibility in lambda calculus demonstrates, it is convenient to be able to ignore some representational issues when talking about "identical" terms in the greater theory. it would help to do the same here, and distinguish between a syntactic and a semantic equivalence of types, where the latter includes and extends the former: syntactic: alpha-conversion, permutation of contexts, probably type synonym expansion (because they are treated as syntactic macros, outside the theory) semantic: type family reduction, .. i'm tempted to the conclusion that the inability of the current system to check its inferred signatures means that reflexivity (of type subsumption/equivalence) is violated: if two types are the same, they should be equivalent and subsume each other. i can't see how the theory can work without this?
However, the fact that we cannot decide type subsumption for ambiguous types is exactly what led us to the original problem. So, nothing has been won.
imho, the trick is to separate syntactic and semantic equivalence, even if we include some "modulo theory" in the former. both <= and ~ need to include this syntactic equivalence. but syntactic equivalence should remain straightforward to check - nothing should be included in it that isn't easily checkable. claus ps i hope it is obvious that i'd like infered signatures to be checkable, not non-checkable signatures to be rejected?-)