Optimization + adding an INLINE pragma triggers Core Lint error (Type of case alternatives not the same as the annotation on case)
Here's a seemingly innocuous program, minimized from the kan-extensions library:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
newtype Curried g h a =
Curried { runCurried :: forall r. g (a -> r) -> h r }
instance Functor g => Functor (Curried g h) where
fmap f (Curried g) = Curried (g . fmap (.f))
instance (Functor g, g ~ h) => Applicative (Curried g h) where
pure a = Curried (fmap ($a))
Curried mf <*> Curried ma = Curried (ma . mf . fmap (.))
{-# INLINE (<*>) #-}
-- The Core Lint error goes away if you remove this INLINE pragmaHowever, it triggers a Core Lint error on GHC 8.2.2 through HEAD if you compile it with -O and -dcore-lint:
$ /opt/ghc/8.6.3/bin/ghc -fforce-recomp -dcore-lint Bug.hs -O
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: (case heq_sel
@ (* -> *)
@ (* -> *)
@ h_a1eC
@ h_a1eC
($d~_a1eE
`cast` (((~) <* -> *>_N co_a1hx <h_a1eC>_N)_R ; N:~[0]
<*
-> *>_N <h_a1eC>_N <h_a1eC>_N
:: (g_a1eB ~ h_a1eC) ~R# (h_a1eC ~~ h_a1eC)))
of co_X1ij
{ __DEFAULT ->
(\ (@ a_a1fg)
(@ b_a1fh)
(ds_d1yw :: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh))
(ds_d1yx :: Curried h_a1eC h_a1eC a_a1fg)
(@ r_a1fn) ->
let {
g_X1zi
:: h_a1eC (b_a1fh -> r_a1fn)
-> h_a1eC ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}]
g_X1zi
= fmap
@ h_a1eC
($dFunctor_a1eD
`cast` ((Functor co_a1hx)_R
:: Functor g_a1eB ~R# Functor h_a1eC))
@ (b_a1fh -> r_a1fn)
@ ((a_a1fg -> b_a1fh) -> a_a1fg -> r_a1fn)
(. @ b_a1fh @ r_a1fn @ a_a1fg) } in
\ (x_X1zn :: h_a1eC (b_a1fh -> r_a1fn)) ->
(ds_d1yx
`cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg>_N
:: Curried h_a1eC h_a1eC a_a1fg
~R# (forall r. h_a1eC (a_a1fg -> r) -> h_a1eC r)))
@ r_a1fn
((ds_d1yw
`cast` (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <a_a1fg -> b_a1fh>_N
:: Curried h_a1eC h_a1eC (a_a1fg -> b_a1fh)
~R# (forall r.
h_a1eC ((a_a1fg -> b_a1fh) -> r) -> h_a1eC r)))
@ (a_a1fg -> r_a1fn) (g_X1zi x_X1zn)))
`cast` (forall (a :: <*>_N) (b :: <*>_N).
<Curried h_a1eC h_a1eC (a -> b)>_R
->_R <Curried h_a1eC h_a1eC a>_R
->_R Sym (N:Curried[0] <h_a1eC>_R <h_a1eC>_R <b>_N)
:: (forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a
-> forall r. h_a1eC (b -> r) -> h_a1eC r)
~R# (forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b))
})
@ b_a1gi
@ b_a1gi
((<$
@ (Curried g_a1eB h_a1eC)
($dFunctor_s1zH
`cast` ((Functor (Curried (Sym co_a1hx) <h_a1eC>_N)_N)_R
:: Functor (Curried h_a1eC h_a1eC)
~R# Functor (Curried g_a1eB h_a1eC)))
@ (b_a1gi -> b_a1gi)
@ a_a1gh
(breakpoint @ b_a1gi)
a1_a1z1)
`cast` (Sym (Curried
(Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi -> b_a1gi>_N)_R
:: Curried g_a1eB h_a1eC (b_a1gi -> b_a1gi)
~R# Curried h_a1eC h_a1eC (b_a1gi -> b_a1gi)))
(a2_a1z2
`cast` (Sym (Curried (Sub (Sym co_a1hx)) <h_a1eC>_R <b_a1gi>_N)_R
:: Curried g_a1eB h_a1eC b_a1gi ~R# Curried h_a1eC h_a1eC b_a1gi))
Type of case alternatives not the same as the annotation on case:
Actual type: forall a b.
Curried h_a1eC h_a1eC (a -> b)
-> Curried h_a1eC h_a1eC a -> Curried h_a1eC h_a1eC b
Annotation on case: forall a b.
Curried g_a1eB h_a1eC (a -> b)
-> Curried g_a1eB h_a1eC a -> Curried g_a1eB h_a1eC bThe size of the -dcore-lint output is enormous, so I'll post it separately as an attachment.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |