GADT type argument not being used for typeclass resolution

Question

Consider the following code

data Foo f where
  Foo :: Foo Int

class DynFoo t where
  dynFoo :: Foo f -> Foo t

instance DynFoo Int where
  dynFoo Foo = Foo

obsFoo :: (DynFoo t) => Foo f -> Foo t
obsFoo = dynFoo

useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> Foo) = 1

The pattern match in useDynFoo should constrain the use of obsFoo to have type Foo f -> Foo Int, which should cause it to search for an instance of DynFoo Int. However, it instead searches for an instance of DynFoo t for unknown t, and naturally fails.

  No instance for (DynFoo t0) arising from a use of ‘obsFoo’
    The type variable ‘t0’ is ambiguous

However, if I change the definition of useDynFoo to

useDynFoo :: Foo f -> Int
useDynFoo (obsFoo -> (Foo :: Foo Int)) = 1

Then it suddenly works, even though my type signature is completely redundant.

So, why is this happening, and how can I use obsFoo without having to give a type signature?

Answer 1

It's clearer if you write it out with an explicit case (view patterns are pretty obscuring WRT type-information flow):

useDynFoo :: Foo f -> Int
useDynFoo foof = case obsFoo foof of
    Foo -> 1

Here, the information f ~ Int is perfectly accessible for the 1. Well, but that's not where we need this information: we need it already at obsFoo foof. And the information can't get there: GADT pattern matches act as a complete “type information diode”, i.e. any information from the outside can be used within the matching scope, but no information from inside can be used without. (For good reasons obviously, because that information can only be confirmed at runtime, when you actually have a GADT constructor to take it from.)

The more interesting question is, why does it work if you add the :: Foo Int signature? Well, that in particular is a weirdness of the view pattern. See, the following would not work:

useDynFoo :: Foo f -> Int
useDynFoo foof = case obsFoo foof of
    (Foo :: Foo Int) -> 1

This information, as you said yourself, is completely redundant.

However it turns out that this view pattern is actually equivalent to putting the signature on the other part of the case:

useDynFoo :: Foo f -> Int
useDynFoo foof = case obsFoo foof :: Foo Int of
    Foo -> 1

and this is quite a different pair of shoes, because now the Foo Int is not inside the GADT pattern match.

I don't know why view pattern with signatures desugar like this, perhaps to make this very pattern possible.

Answer 2

Type signatures are not redundant when using GADTs. Note the final bullet point of GHC Users Guide: GADTs