assertSameLength exception that appears anomalous

[jazullo]

Consider this code
It yields the error

~/gibbon$ cabal v2-exec gibbon -- --packed --no-gc --to-exe ../llrbt/rbtree_correct2.hs
gibbon: assertSameLength: Type applications [ArrowTy [IntTy] IntTy] incompatible with the type variables: [succ,identity_595].
 While lowering the expression AppE "map_opt_596"
     []
     [IfE (AppE "unB" [] [VarE "c_270"])
          (Ext (FunRefE [] "identity_595"))
          (Ext (FunRefE [] "succ")),
      AppE "meet"
           []
           [AppE "check_bh" [] [VarE "l_272"],
            AppE "check_bh" [] [VarE "r_273"]]]
CallStack (from HasCallStack):
  error, called at src/Gibbon/L0/Specialize2.hs:410:8 in gibbon-0.2-inplace:Gibbon.L0.Specialize2
  assertSameLength, called at src/Gibbon/L0/Specialize2.hs:1017:15 in gibbon-0.2-inplace:Gibbon.L0.Specialize2

Examining

identity :: a -> a
identity x = x

succ :: Int -> Int
succ x = x + 1

map_opt :: (a -> b) -> Maybe a -> Maybe b
map_opt f m = case m of
  Just x -> Just (f x)
  Nothing -> Nothing

meet :: Maybe Int -> Maybe Int -> Maybe Int
meet m1 m2 = case m1 of
  Nothing -> Nothing
  Just x -> case m2 of
    Nothing -> Nothing
    Just y -> if x == y then m1 else Nothing

-- assert both subtrees have equal black heights
check_bh :: RBT -> Maybe Int
check_bh t = case t of
  Empty -> Just 1
  Node c x l r -> 
    map_opt (if unB c then identity else succ) (meet (check_bh l) (check_bh r))

(meet (check_bh l) (check_bh r)) clearly produces a Maybe Int. The if expression produces a function with mgu Int -> Int. I am not sure what the issue is with this code.