Type class problem

[Carl Witty]

On Thu, 2003-08-28 at 13:10, Brandon Michael Moore wrote:
> Unfortunately I don't have a useful syntatic condition on instance
> declarations that insures termination of typechecking. If types are
> restriced to products, sums, and explicit recursion, then termination is
> ensured if we restrict the assumtions of a declaration to instances for
> subexpressions of the type we are declaring an instance for (there are
> only a finite number of subexpressions times a finite number of classes,
> and one is added each time we apply a rule). I haven't made any progress
> if type operators are allowed, and I don't have any simple check whether a
> Haskell type expression can be represented without type operators. I
> was hoping to get normalization of type expressions from the simple
> kinding, but recursive operator definitions break that.

I think some of David McAllester's papers from about 1990-1994 may be
relevant here.  He has several papers on deciding when sets of inference
rules are terminating, or terminating in polynomial time.  (He applies
this in the context of automated theorem proving, but it should apply
perfectly well to type class inference as well.)

Carl Witty