[Haskell-cafe] GADT/Typeable/existential behaviour that I don't understand

[Tom Ellis]

I can define the following

    import Data.Typeable
    data Foo where Foo :: Typeable x => x -> Foo
    eq = (\a b -> eqT) :: (Typeable a, Typeable b) => a -> b -> Maybe (a :~: b)

and then these expressions work as expected


> case Foo "Hello" of Foo x1 -> case eq x1 "" of { Nothing -> "It was not a string"; Just Refl -> "It was a string" }

"It was a string"

> case Foo 1 of Foo x1 -> case eq x1 "" of { Nothing -> "It was not a string"; Just Refl -> "It was a string" }
"It was not a string"


But if I omit the 'Nothing' branch (as below) I get "Couldn't match
expected type ‘p’ with actual type ‘[Char]’ ‘p’ is untouchable".

Can anyone explain why this happens?


> case Foo "Hello" of Foo x1 -> case eq x1 "" of { Just Refl -> "It was not a string" }
> case Foo 1       of Foo x1 -> case eq x1 "" of { Just Refl -> "It was not a string" }