[Haskell-cafe] Re: Typechecker to GADT: the full implementation of a typed DSL

[Ryan Ingram]

On 10/7/07, Ryan Ingram <ryani.spam at gmail.com> wrote:
> On 10/4/07, Pasqualino 'Titto' Assini <tittoassini at gmail.com> wrote:
> > My mental typechecker seems to diverge on the  "data EQ a b where  Refl :: EQ
> > a  a" bit so I am now reading the "typing dynamic typing" paper, hoping for
> > further enlightment.
>
> Basically, if you have "Refl :: Eq a b", it provides a witness that
> the types a and b are really the same type.

Also, something that might make it simpler to understand is that the
"a" and "b" in the initial GADT declaration are irrelevant (and
totally ignored).  Here is an equivalent definition:

data EQ :: * -> * -> * where Refl :: EQ a a

  -- ryan