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:

1. 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!
2. 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