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
inM_Ranked
is essential: if it is removed, all fourbar
s are accepted. - The
M_Nest
case ofMixed
is essential: idem. - The
False
inM_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])