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