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

[Adam Gundry]

On 21/07/2020 08:13, Tom Ellis wrote:
> 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" }

Sure, that's a nice simple example, and shows that the crucial aspect is
really the GADT pattern match. Let's recall the definition of type
equality (modulo details):

    data a :~: b where
        Refl :: (a ~ b) => a :~: b

There aren't any existential type variables here, just an equality
constraint, which will be "provided" when pattern-matching on `Refl`.

In both your examples, type inference determines that the type of the
expression must be `Maybe (a :~: b) -> p` for some as-yet-unknown `a`,
`b` and `p`. The RHSs of the patterns must then be used to determine
`p`. But if all we have is

    \case { Just Refl -> "Same" }

then the pattern-match on `Just Refl` introduces a given constraint `a ~
b` and we need to solve `p ~ String` under that assumption. The presence
of the assumption means that simply unifying `p` with `String` isn't
necessarily correct (more precisely, it isn't necessarily a unique most
general solution). Thus type inference must refrain from unifying them.
If the assumption isn't present (as in the `Nothing` case), it can just
go ahead and unify.

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.

Does this make things clearer?

Adam


> 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