[Haskell] Conditional typechecking with GADTs

[Taral]

On 12/27/05, oleg at pobox.com <oleg at pobox.com> wrote:
> data a  :+: bb                          -- Conj assertion a and assertions bb
> data aa :@: bb                          -- Conjunction of assertions aa and bb

Why is the difference here?

> class WellTyped a
> instance WellTyped Nil
> instance WellTyped cs => WellTyped ((a :=: a) :+: cs)
> instance (WellTyped cs1, WellTyped cs2) => WellTyped (cs1 :@: cs2)

Could one not write:

instance WellTyped (a :=: a)

and do away with (:+:)?

--
Taral <taralx at gmail.com>
"Computer science is no more about computers than astronomy is about
telescopes."
    -- Edsger Dijkstra