Tue Jul 21 07:13:26 UTC 2020

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