Strange inference behaviour with Coercible + data families

Summary

This is a regression in 9.8: the code below works fine in 9.2.8, 9.4.8 and 9.6.5, but fails in 9.8.2 and 9.10.1.

One can contrive to make let r = g x in f r pass typechecking whereas f (g x) fails. I'm writing this issue under the assumption that such behaviour is undesirable in general; if it is considered acceptable in this case (especially because the issue can also be eliminated using some type applications on f), feel free to close.

Unfortunately I have not been able to reduce the code in question to something smaller than this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Array.Nested.Internal where

import Data.Coerce (coerce)


type family Id (b :: Bool) where
  Id b = b

newtype Ranked b a = MkRanked (Mixed b a)


data family Mixed (b :: Bool) a

newtype instance Mixed b1 (Mixed b2 a) = M_Nest (Mixed False a)

newtype instance Mixed b (Ranked c a) = M_Ranked (Mixed b (Mixed (Id c) a))


idMixed :: Mixed b a -> Mixed b a
idMixed = undefined

bar :: Mixed b (Ranked c a) -> Mixed b (Ranked c a)
bar (M_Ranked @_ @c @a arr)
  = coerce (idMixed arr)                          -- fails
  -- = coerce (idMixed @_ @(Mixed (Id c) a) arr)  -- ok
  -- = coerce (id arr)                            -- ok
  -- = let r = idMixed arr in coerce r            -- ok

Play with it here: https://play.haskell.org/saved/qSTX6YZe

Diagnostics from GHC 9.8.2 on the program as written:

Details box

input.hs:26:5: error: [GHC-25897]
    • Couldn't match type ‘b’ with ‘False’
        arising from a use of ‘coerce’
      ‘b’ is a rigid type variable bound by
        the type signature for:
          bar :: forall (b :: Bool) (c :: Bool) a.
                 Mixed b (Ranked c a) -> Mixed b (Ranked c a)
        at input.hs:24:1-51
    • In the expression: coerce (idMixed arr)
      In an equation for ‘bar’:
          bar (M_Ranked @_ @c @a arr) = coerce (idMixed arr)
    • Relevant bindings include
        arr :: Mixed b (Mixed (Id c) a) (bound at input.hs:25:24)
        bar :: Mixed b (Ranked c a) -> Mixed b (Ranked c a)
          (bound at input.hs:25:1)
   |
26 |   = coerce (idMixed arr)                          -- fails
   |     ^^^^^^

input.hs:26:21: error: [GHC-25897]
    • Couldn't match type ‘a’ with ‘Mixed c a’
      Expected: Mixed b a
        Actual: Mixed b (Mixed (Id c) a)
      ‘a’ is a rigid type variable bound by
        the type signature for:
          bar :: forall (b :: Bool) (c :: Bool) a.
                 Mixed b (Ranked c a) -> Mixed b (Ranked c a)
        at input.hs:24:1-51
    • In the first argument of ‘idMixed’, namely ‘arr’
      In the first argument of ‘coerce’, namely ‘(idMixed arr)’
      In the expression: coerce (idMixed arr)
    • Relevant bindings include
        arr :: Mixed b (Mixed (Id c) a) (bound at input.hs:25:24)
        bar :: Mixed b (Ranked c a) -> Mixed b (Ranked c a)
          (bound at input.hs:25:1)
   |
26 |   = coerce (idMixed arr)                          -- fails
   |                     ^^^

The expected behaviour is that all four definitions of bar are equivalent, especially given that the fourth does indeed succeed.

I'm not sure what is going on here. Note that:

• The Id in M_Ranked is essential: if it is removed, all four bars are accepted.
• The M_Nest case of Mixed is essential: idem.
• The False in M_Nest doesn't matter: different values give various different errors. This is suspicious because it should not matter at all: M_Nest is never constructed in this program.

Environment

• GHC version used: 9.8.2, 9.10.1 (code typechecks normally in [9.2 .. 9.6.5])