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