GADT question

[Andres Loeh]

> > 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