Core Lint error when using record update with GADT in data family
The following module leads to a Core Lint error in both 8.10.2 and HEAD. I came across this in the context of !3257.
{-# LANGUAGE GADTs, TypeFamilies #-}
{-# OPTIONS_GHC -dcore-lint #-}
module Bug where
data family F s t
data instance F s t where
MkF :: { foo :: Int } -> F Int t
bar :: F s t -> Int -> F s t
bar z y = z {foo = y}
Specifically the error is:
$ ghc-8.10.2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
Bug.hs:14:7: warning:
From-type of Cast differs from type of enclosed expression
From-type: R:Fst Int t_auE
Type of enclosed expression: F Int t_auE
Actual enclosed expression: $WMkF @ t_auE ds_dv6
Coercion used in cast: (R:Fst (Sym ds_dv7) <t_auE>_N)_R
In the RHS of bar :: forall s t. F s t -> Int -> F s t
In the body of lambda with binder s_auD :: *
In the body of lambda with binder t_auE :: *
In the body of lambda with binder z_atK :: F s_auD t_auE
In the body of lambda with binder y_atL :: Int
In the body of letrec with binders ds_dv6 :: Int
In the body of letrec with binders ds_dv9 :: R:Fst s_auD t_auE
In a case alternative: (MkF ds_dv7 :: s_auD ~# Int, ds_dv8 :: Int)
Substitution: [TCvSubst
In scope: InScope {wild_00 z_atK y_atL s_auD t_auE $krep_av2
$krep_av3 $krep_av4 $krep_av5 ds_dv6 ds_dv7 ds_dv8 ds_dv9
foo bar $tcF $tc'MkF $trModule}
Type env: []
Co env: [dv7 :-> ds_dv7]]