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