How does GADTs affect type inference in this case?

Question

Say I have a monad that emits soft failure through Writer. A simplified version goes like this (for the record, I'm using GHC 9.0.2):

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
-- {-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lib where

import Control.Monad.Writer.CPS
import Data.Maybe

verify :: MonadWriter [String] m => some -> args -> m ()
verify _ _ = fix \(_ :: m ()) ->
  do
    let warn = tell . (: [])
        a = Just 1 :: Maybe Int
        b = Just [1, 23] :: Maybe [Int]
        c = Just (id :: forall a. a -> a)
        -- isJust' :: String -> Maybe a -> m ()
        isJust' tag v = unless (isJust v) do
          warn $ tag <> " is Nothing"
    isJust' "a" a
    isJust' "b" b
    isJust' "c" c

All goes fine until I add GADTs extension, then GHC fails to find the most general type for isJust':

    • Couldn't match type ‘[Int]’ with ‘Int’
      Expected: Maybe Int
        Actual: Maybe [Int]
    • In the second argument of ‘isJust'’, namely ‘b’
      In a stmt of a 'do' block: isJust' "b" b
      In the expression:
        do let warn = tell . (: [])
               a = ...
               ....
           isJust' "a" a
           isJust' "b" b
           isJust' "c" c
   |
22 |     isJust' "b" b
   |                 ^

/var/tmp/demo/src/Lib.hs:23:17: error:
    • Couldn't match type ‘a0 -> a0’ with ‘Int’
      Expected: Maybe Int
        Actual: Maybe (a0 -> a0)
    • In the second argument of ‘isJust'’, namely ‘c’
      In a stmt of a 'do' block: isJust' "c" c
      In the expression:
        do let warn = tell . (: [])
               a = ...
               ....
           isJust' "a" a
           isJust' "b" b
           isJust' "c" c
   |
23 |     isJust' "c" c
   |                 ^

At which point I have to uncomment type annotation for isJust' to get this to type check - I'm wondering what is at play here, I don't think I'm using any GADTs features?

Side note 1: I usually just slam a NoMonomorphismRestriction to see if it helps, it didn't.

Side note 2: That use of fix is just for getting a hold on that m in the presence of ScopedTypeVariables - a side question is whether there are better ways to do this without relying on verify having an explicit type signature (say this function is defined inside an instance).

Answer 1

The problem is not GADTs but MonoLocalBinds, which is automatically enabled by GADTs. The issue is that isJust' :: String -> Maybe a -> m () has a polymorphic type signature, meaning you get to choose what a is every time you call it. At least, it would be polymorphic if MonoLocalBinds wasn't enabled. Per the documentation:

With MonoLocalBinds, a binding group will be generalised if and only if

• It is a top-level binding group, or
• Each of its free variables (excluding the variables bound by the group itself) is closed (see next bullet), or
• Any of its binders has a partial type signature (see Partial Type Signatures).

If a variable does not satisfy one of the three bullets, its type is not generalized, i.e. it does not get to be polymorphic.

There is a rigorous definition of what a "closed variable" is, but the important part is:

if a variable is closed, then its type definitely has no free type variables.

The second argument of isJust' has type Maybe a for some unknown a, meaning it is not closed (edit: see Li-yao Xia's correction in the comments). So, bullet 1 is not satisfied because isJust' is defined within verify, bullet 2 is not satisfied because the second argument of isJust' is not closed, and bullet 3 is not satisfied because there are no holes in the type of isJust'. Thus, isJust' is not polymorphic after all.

All this means is that the a in String -> Maybe a -> m () is actually a fixed type that GHC has to infer. It sees you call isJust' "a" (a::Maybe Int) and assumes a ~ Int, but then it sees isJust' "b" (b::Maybe [Int]) and assumes a ~ [Int] as well. Obviously this is a problem, so GHC complains. The only thing adding the type signature does is tell GHC to make isJust' polymorphic.

Note that you can have GADTs and NoMonoLocalBinds at the same time, but because type inference with GADTs is tricky this will probably just cause more problems when you actually use GADTs.