I get an error "No instance for (Fractional a) arising from the use of '/'" This seems odd to me, since Div is constrained to have fractional arguments. Is there something obvious I'm missing?
Unless GADTs are handled specially, and I don't think they are in this case, this problem is not specific to GADTs but related to how type constraints on constructors are handled in general. Basically, a constraint on a constructor has no effect beyond beyond constraining what the constructor can be applied to (see the Haskell 98 report 4.2.1). In particular, when you take a constructed value apart through pattern matching, the constraints do not come into play: hence the "no instance" message.
I think this is the correct explanation. However, it might be confusing that IsZ :: Num a => Term a -> Term Bool and eval (IsZ t) = eval t == 0 works correctly. The difference here is that for IsZ, the compiler will store a Num dictionary within the constructed value, because a is existentially quantified. On the other hand, in Div :: Fractional a => Term a -> Term a -> Term a the a is visible on the outside, so the compiler does not store a dictionary. But then, while computing the pattern match eval (Div t u) = eval t / eval u there's really no way to create one. So, the question is, why cannot the compiler treat the case for Div more like the case for IsZ and store the Fractional dictionary within the constructor?
It has been suggested a number of times that constraints on constructors should have a more profound meaning, and maybe GADTs make this even more desirable, as your example suggest.
I think they do. Maybe the work that has already been done on GADTs and existentials finally make it possible to give an improved semantics to constraints on datatypes without too much additional work. Cheers, Andres