Pathological type family turns type error into runtime loop
If I say
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
import Data.Proxy
type family F a where
F a = F (F a)
foo :: Proxy (F Bool) -> Proxy (F Int)
foo x = x
main = print $ foo Proxy
and compile, compilation succeeds, and I get Proxy
when I run the resulting program. This is unexpected, but perhaps reasonable given the perverseness of F
. (I would expect compilation to loop or to otherwise fall over.) But, what's really scary is the Core (from -ddump-simpl
):
<snip>
Rec {
cobox6_rZA :: Main.F GHC.Types.Bool ~ GHC.Prim.Any
[GblId, Str=DmdType]
cobox6_rZA =
case cobox6_rZA of _ [Occ=Dead] { GHC.Types.Eq# cobox9_dYJ ->
case cobox5_rZz of _ [Occ=Dead] { GHC.Types.Eq# cobox11_dYK ->
GHC.Types.Eq#
@ *
@ (Main.F GHC.Types.Bool)
@ GHC.Prim.Any
@~ (Main.TFCo:R:F[0] <GHC.Types.Bool>_N
; (Main.F cobox9_dYJ)_N
; cobox11_dYK)
}
}
end Rec }
<snip>
Main.main :: GHC.Types.IO ()
[GblId, Str=DmdType]
Main.main =
System.IO.print
@ (Data.Proxy.Proxy GHC.Prim.Any)
(Data.Proxy.$fShowProxy @ * @ GHC.Prim.Any)
(case cobox7_rZB of _ [Occ=Dead] { GHC.Types.Eq# cobox9_dYG ->
case cobox3_rZx of _ [Occ=Dead] { GHC.Types.Eq# cobox11_dYV ->
case cobox6_rZA of _ [Occ=Dead] { GHC.Types.Eq# cobox13_dYC ->
Data.Proxy.Proxy @ * @ GHC.Prim.Any
}
}
})
<snip>
main
forces cobox6_rZA
. cobox6_rZA
forces... cobox6_rZA
! And yet, this program does not loop when run. This is deeply troubling.
So, I see (at least) 2 bugs here:
- It seems to me that the core program, while seemingly well-formed (
-dcore-lint
does not complain) should loop when run, according to my understanding of its operational semantics. And yet it doesn't! - We should probably never even produce Core like this, though I'm willing to allow for the possibility that we can blame the programmer.
Or, have I horribly misunderstood something?
(Credit to Dominic Orchard for coming up with this.)
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |
Edited by Richard Eisenberg