Why haskell can't infer type for this GADT

Question

Simple GADT:

data GADT a  where
    MkGADT :: Int -> GADT Int

And function without type signature, with error:

ghci> inferGADT (MkGADT n) = "123"

<interactive>:14:24: error:
    • Could not deduce: p ~ String
      from the context: a ~ Int
        bound by a pattern with constructor: MkGADT :: Int -> GADT Int,
                 in an equation for ‘inferGADT’
        at <interactive>:14:12-19
      ‘p’ is a rigid type variable bound by
        the inferred type of inferGADT :: GADT a -> p
        at <interactive>:14:1-28
      Possible fix: add a type signature for ‘inferGADT’
    • In the expression: "123"
      In an equation for ‘inferGADT’: inferGADT (MkGADT n) = "123"
    • Relevant bindings include
        inferGADT :: GADT a -> p (bound at <interactive>:14:1)

If I provide type signature - it's ok:

inferGADT ((MkGADT n)::(GADT Int)) = "123"
ghci> :t inferGADT 
inferGADT :: GADT Int -> String

If i define term like this, haskell can infer type:

ghci> :t (MkGADT 1)
(MkGADT 1) :: GADT Int

In first case I do pattern matching, in second - just use constructor to build value. Why haskell can't infer type in first case? For me it's look strange because I think all information needed to infer type is presented in MkGADT constructor, it explicitly show that MkGADT :: Int -> GADT Int

ps. From error message as I understand that it find that a ~ Int and "Could not deduce: p ~ String", why? - function definition given is just string "123"..

This is confusing, what happens here during type inference?

Answer 1

There are at least two incomparable types:

type family F a
type instance F Int = String
type instance F Char = ()

inferGADT :: GADT a -> String
inferGADT :: GADT a -> F a

Neither of these is a more general type than the other: taking a ~ Char in each these specialize to GADT Char -> String and GADT Char -> (). In fact, there is no type which is more general than all the other types that can be given to inferGADT.

So type inference fails, and demands that you tell it which of the incomparable types you want.