Thanks, your example is much simpler and clearer, and shows it has nothing to do with the GADT "Foo". But I'm confused about the relevance of `x1 :: t`. In fact the following example is even simpler and clearer and doesn't mention `eq` at all. Could you explain why the existential that comes from matching on Refl means that the return value cannot be inferred as `String`? * Works \case { Just Refl -> "Same"; Nothing -> "Different" } * Does not work \case { Just Refl -> "Same" } On Mon, Jul 20, 2020 at 09:03:14PM +0100, Adam Gundry wrote:
In fact, if we consider just
case eq x1 "" of { Just Refl -> "It was not a string" }
in isolation, and suppose `x1 :: t`, this can be given two incomparable most general types, namely `String` and `t`. So type inference refuses to pick, even though in your case only `String` would work out later, but seeing that requires non-local reasoning about escaped existentials.
On 20/07/2020 19:18, Tom Ellis wrote:
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" }
-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/
Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.