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

[Tom Ellis]

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.