Type families interfere with specialisation rewrite rules
Consider the attached file, in particular the function
vinr :: Length as -> VSum bs -> VSum (as ++ bs)
its specialised version
vinr0 :: Length '[] -> VSum as -> VSum as
and the rewrite rule
{-# RULES "vinr/0" vinr = vinr0 #-}
According to the relevant section of GHC user guide, vinr
should be replaced with vinr0
whenever the types match. However, the resulting Core for test
contains the following (compiled with ghc -O2
):
Test.test1
= case extractIdx
@ 'Z @ '[Int] @ Int (Test.$WIZ @ Int @ '[]) Test.test2
of {
Left other_aZf ->
Test.$wvinl @ Length @ '[Int] @ (Remove 'Z '[Int]) other_aZf;
Right x_aZg ->
vinr
@ (Remove 'Z '[Int])
@ '[Int]
(Test.$WLZ
`cast` ((Length (Sym (Test.D:R:Remove[0] <Int>_N <'[]>_N)))_R
:: (Length '[] :: *) ~R# (Length (Remove 'Z '[Int]) :: *)))
(Test.VInL
@ '[Int]
@ Int
@ '[]
@~ (<'[Int]>_N :: ('[Int] :: [*]) GHC.Prim.~# ('[Int] :: [*]))
x_aZg)
}
So the rule never fires, and vinr
is still there, even though it is directly applied to LZ :: Length '[]
.
My dilettante analysis is that, for some reason, GHC keeps the Remove 'Z '[Int]
as-is, not evaluating it to '[]
, and, since the types don't match //syntactically//, doesn't apply the rule. In particular, if I replace type families with classes with functional dependencies, the rule fires as expected.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |