How does GHC infer the intended type for this GADT?

My understanding of GHC type inference was that in the absence of type annotations, it will default to Hindley-Milner. However, to my pleasant surprise GHC infers Num p => G a -> p for f as opposed to Num p => G Char -> p.

data G a where
  A :: a      -> G a
  B :: String -> G Char

f (A a) = 42
f (B s) = 24

My question is how does it do this and under what other situations it will infer the correct type for a GADT?

Solution

GHC “disables” Hindley-Milner in GADT pattern matching, so as to prevent dynamic type information from escaping its scope.

Here's a more extreme example:

import Data.Void

data Idiotic :: * -> * where
  Impossible :: !Void -> Idiotic Void
  Possible :: a -> Idiotic a

There don't exist any values of type Void, so it isn't possible to ever use the Impossible constructor. Thus, Idiotic a is actually isomorphic to Identity a, IOW to a itself. So, any function that takes an Idiotic value is fully described by just the Possible pattern match. Basically, it always boils down to

sobre :: Idiotic a -> a
sobre (Possible a) = a

which is easy usable in practice.

But as far as the type system is concerned, the other constructor matches just as well, and is in fact required to disable the incomplete pattern warning:

sobre (Impossible a) = {- Here, a::Void -} a

But if the compiler propagated this type information outwards, your function would end up with the completely useless signature

sobre :: Idiotic Void -> Void