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

[Tom Ellis]

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