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" }