[Haskell-cafe] Putting constraints on "internal" type variables in GADTs

[Tillmann Rendel]

Hi,

Anupam Jain wrote:
> -- My datatype
> data T o where
>    Only ∷ o → T o
>    TT ∷ T o1 → (o1 → o2) → T o2
>
> -- Show instance for debugging
> instance Show o ⇒ Show (T o) where
>    show (Only o) = "Only " ⊕ (show o)
>    show (TT t1 f) = "TT (" ⊕ (show t1) ⊕ ")"

As you noticed, the last line doesn't work because t1 is of some unknown 
type o1, and we know nothing about o1. In particular, we don't know how 
to show values of type t1, neither at compile time nor at runtime. I 
can't see a way around that.

However, for debugging, you could do:

   show (TT t1 f) = "TT (" ++ show (f t1) ++ ")"

This is not perfect, but at least it should work.

   Tillmann