Comment GHC déduit-il le type prévu pour ce GADT ?

Question

Ma compréhension de l'inférence de type GHC était qu'en l'absence d'annotations de type, il utilisera par défaut Hindley-Milner. Cependant, à mon agréable surprise, GHC infère Num p => G a -> p pour f à l'opposé de 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

Ma question est de savoir comment il procède et dans quelles autres situations il va déduire le type correct pour un GADT ?

Answer 1

GHC "désactive" Hindley-Milner dans le filtrage GADT, afin d'empêcher les informations de type dynamique d'échapper à leur portée.

Voici un exemple plus extrême :

import Data.Void

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

Il n'existe pas de valeurs de type Void Il n'est donc jamais possible d'utiliser la fonction Impossible Constructeur. Ainsi, Idiotic a est en fait isomorphe à Identity a , IOW à a même. Ainsi, toute fonction qui prend un Idiotic est entièrement décrite par la seule valeur Possible correspondance du modèle. En gros, cela se résume toujours à

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

ce qui est facilement utilisable en pratique.

Mais en ce qui concerne le système de type l'autre constructeur correspond tout aussi bien, et est en fait nécessaire pour désactiver l'option incomplete pattern avertissement :

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

Mais si le compilateur propageait cette information de type vers l'extérieur, votre fonction se retrouverait avec la signature complètement inutile

sobre :: Idiotic Void -> Void