GADT's: Is there a reason why the weakest or strongest type is not chosen

Question

I'm reading Fun With Phantom Types. The first exercise asks why it is necessary to provide a signature to functions operating on Phantom Types. While I cannot come up with a general reason, I do see a problem in the following example:

data Expr a where
  I :: Int -> Expr Int
  B :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  Eq :: (Eq a) => Expr a -> Expr a -> Expr Bool


whatIs (I _) = "an integer expression"
whatIs (Add _ _) = "an adition operation"

Now I understand that there are two possible types for whatIs above, namely:

Expr a -> String

and

Expr Int -> String

however, the compiler instead gives an error:

• Couldn't match expected type ‘t’ with actual type ‘[Char]’
    ‘t’ is untouchable
      inside the constraints: t1 ~ Int
      bound by a pattern with constructor: I :: Int -> Expr Int,
               in an equation for ‘whatIs’
      at ti.hs:9:9-11
  ‘t’ is a rigid type variable bound by
    the inferred type of whatIs :: Expr t1 -> t at ti.hs:9:1
  Possible fix: add a type signature for ‘whatIs’
• In the expression: "someString"
  In an equation for ‘whatIs’: whatIs (I _) = "someString"
• Relevant bindings include
    whatIs :: Expr t1 -> t (bound at ti.hs:9:1)

I'm wondering why the compiler does not choose any of the two.

Answer 1

For your example, Expr a -> String is a strictly better type than Expr Int -> String: anywhere that an Expr Int -> String could be used, an Expr a -> String will certainly do. But sometimes there isn't a "weakest" or "strongest" type.

Let's simplify your example even further:

data SoSimple a where
    SoSimple :: SoSimple Int

eval SoSimple = 3 :: Int

Now here are two perfectly good types to give eval:

eval :: SoSimple a -> a
eval :: SoSimple a -> Int

These types aren't interchangeable! Each is useful in different situations. Compare:

{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
import Data.Void

data SomeSimple where
    SomeSimple :: SoSimple a -> SomeSimple

-- typechecks if eval :: SoSimple a -> Int,
--    but not if eval :: SoSimple a -> a
evalSome :: SomeSimple -> Int
evalSome (SomeSimple x) = eval x

-- typechecks if eval :: SoSimple a -> a,
--    but not if eval :: SoSimple a -> Int
evalNone :: SoSimple Void -> Void
evalNone = eval

So neither of these is more general than the other (and it turns out that no type is more general than both while still letting eval itself typecheck). Since there is no most-general type for eval, it makes sense to refuse to pick a type and force the user to decide which of the many possible types they want this time around.