How does GHC infer the intended type for this GADT?

Question

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?

I do not really follow why you think that it should use G Char in the first place? Deriving types typically happens by first using the most generic type, and subsequently replacing types based on elements in the head and body of the function. — Willem Van Onsem
By "how does it do this" what do you mean? Do you want an explanation of Hindley-Milner in this context? — AJF
f does not impose any restrictions on its input, except that it should be G. The function does not analyze a or s any further. The fact that in B can be used for G Char only is irrelevant for deducing f's type. — yeputons
I think the confusion stems from not knowing that the algorithm looks for the most generic matching type. E.g. when looking at f (B s) one could be tempted to think that the argument must have type G Char and not the more general G a. — mschmidt
@yeputons yes, I was under the impression that Char would constrain the type variable. Thanks! — madgen

leftaroundabout leftaroundabout · Accepted Answer · 2018-06-17T10:51:26

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

How does GHC infer the intended type for this GADT?

1 Answers