Why only inference in type checking?

[Philip K.F. Hölzenspies]

Dear Simon,

You mentioned that GHC uses 'checking' when it knows the types. How
this relates to 'unification', I don't know. It might very well be the
same. Hopefully, the following example sheds a bit more light on what
I mean (carefully nicked from Uktaad B'mal's "Beginning Faking It").
Examples are many, including in the "Understanding FDs via CHRs"
paper.

-- Start example

To define 'vectors,' we need to code the length of a list in a type.
With the zero/successor notation for naturals, we can do this is data
constructors without term-level constructors:

data Z
data S x

Vector concatenation requires addition of these numerals. In Prolog
terms:

Add(zero, X, X).
Add(s X, Y, s Z) :- Add X Y Z

We can translate this to a type class as

class Add a b c | a b -> c
instance Add Z x x
instance Add x y z => Add (S x) y (S z)

-- End example

Because of your paper I understand why the coverage condition is in
place and why it fails for the last of these instance declarations.
GHC will allow me to do this by saying allow-undecidable-instances.
As you state in the paper, the three FD-conditions of Coverage,
Consistency and Bound Variable are sufficient, but not (always)
necessary.

I see why the example above causes considerable problems for
inference, but if I read these instance declarations as Horn clauses,
I see no problem at all in checking any actual occurrence in a
program, i.e. if I write a concatenation function for vectors that
uses this class as a property of vectors, I don't see where a type
checker, using Prolog-like unification, runs into difficulties.

What I'm probably asking (it's hard to tell, even for me, sometimes),
is whether there is something between a type checker that is
guaranteed to terminate and throwing all guarantees with regards to
decidability right out the window. Again, I might be completely
mistaken about how GHC does this. In that case I would like to find
out where I make a wrongful assumption.

Regards,
Philip