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

[Adam Gundry]

Hi Tom,

The mention of "untouchable" type variables indicates that this is a
type inference problem, and indeed, if you add a `:: String` type
signature your expression will be accepted. The problem is determining
the type of the whole expression, which is what the unification variable
`p` stands for.

When type-checking pattern-matches on GADTs, the GADT brings new
constraints into scope (e.g. your match on `Just Refl` brings into scope
a constraint that the type of `x1` must be `String`). However, this
means that any constraints that arise under the match cannot be used to
solve for unification variables "outside" the match, because in general
there may be multiple solutions.

In your example, the RHS of the `Just Refl` case leads to a constraint
that `p ~ String`, which cannot be solved directly. When there is a
`Nothing` case, its RHS also leads to a `p ~ String` constraint, this
time not under a GADT pattern match, so `p` gets solved with `String`
and type inference succeeds. But in the absence of the `Nothing` case,
there is no reason for type inference to pick that solution.

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.

Hope this helps,

Adam


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