Skip to content

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]]
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information