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

[Marcin Szamotulski]

Another interesting case:

```
λ :t \case { Just Refl -> undefined; }
\case { Just Refl -> undefined; } :: Maybe (a :~: b) -> p
```

Cheers,
Marcin

‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Tuesday, July 21, 2020 11:19 AM, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> wrote:

> Ah yes! All of the following are valid (i.e. when the type signature
> is provided explicitly).
> 

> -   (\case { Just Refl -> "Same" }) :: Maybe (a :~: b) -> String
> 

> -   (\case { Just Refl -> "Same" }) :: Maybe (String :~: b) -> b
> 

> -   (\case { Just Refl -> "Same" }) :: Maybe (a :~: String) -> a
> 

> Furthermore, both of these are valid
> 

> -   -- inferred :: Typeable p => p -> p
>     \b -> case eq "Hello" b of { Just Refl -> "Same"; Nothing -> b }
>     

> 

> -   -- inferred :: Typeable b => b -> String
>     \b -> case eq "Hello" b of { Just Refl -> "Same"; Nothing -> "Different" }
>     

> 

> So we could fill in the`Nothing` branch with either something of type
> `b` or something of type `String`. If we omit the `Nothing` branch
> and the type signature then the type inference engine has no way to
> know which one we meant! In the earlier examples, `b` was of type
> `String` so they would work out to the same thing (as was my implicit
> expectation), but this requires "non-local reasoning", as you
> mentioned. Parenthetically, I wonder if a "quick look" approach could
> resolve this particular case, but I see that making it work in general
> may be impossible.
> 

> Thanks, Adam, for providing those enlightening examples. When I get
> far enough away from Hindley-Milner I lose the ability to predict how
> these things are going to work but your examples give me some useful
> guidance.
> 

> Tom
> 

> On Tue, Jul 21, 2020 at 09:01:52AM +0100, Adam Gundry wrote:
> [...]
> 

> > The underlying reason for this restriction is that type inference should
> > return principal types (i.e. every possible type of the expression
> > should be an instance of the inferred type). But with GADTs this isn't
> > always possible. Notice that your second case can be given any of the types
> > 

> >     Maybe (a :~: b) -> String
> >     Maybe (a :~: String) -> a
> >     Maybe (String :~: a) -> a
> >     

> > 

> > so it doesn't have a principal type for type inference to find. But when
> > the `Nothing` branch is present, only the first of these types is possible.
> > On 21/07/2020 08:13, Tom Ellis wrote:
> > 

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

> 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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 477 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200724/3262f010/attachment.sig>