GADT/Typeable/existential behaviour that I don't understand
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" }
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
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" } 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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
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
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" }
Another interesting case:
```
λ :t \case { Just Refl -> undefined; }
\case { Just Refl -> undefined; } :: Maybe (a :~: b) -> p
```
Cheers,
Marcin
‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐
On Tuesday, July 21, 2020 11:19 AM, 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" }
Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (3)
-
Adam Gundry -
Marcin Szamotulski -
Tom Ellis