Opened 3 years ago

Closed 3 years ago

Last modified 23 months ago

#9554 closed bug (fixed)

Pathological type family turns type error into runtime loop

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.8.2
Keywords: Cc: jan.stolarek@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_fail/T9554
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (5)

comment:1 Changed 3 years ago by goldfire

Summary: Pathological type family seems to violate FC operational semanticsPathological type family turns type error into runtime loop

Another look at this revealed it's not as bad as I thought: the Show instance for Proxy is lazy in its argument. So, foo was never being evaluated.

But, consider this:

{-# 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 = case foo Proxy of Proxy -> putStrLn "Made it!"

This does properly force foo, and the result is a runtime loop. The core is similar to that in the original post, in that it contains clearly looping coercions.

This is bad: it means that -XUndecidableInstances allows programs to go wrong, contrary to my (and many others') assumptions about -XUndecidableInstances.

comment:2 Changed 3 years ago by jstolarek

Cc: jan.stolarek@… added

comment:3 Changed 3 years ago by Richard Eisenberg <eir@…>

In c1edbdfd9148ad9f74bfe41e76c524f3e775aaaa/ghc:

Do proper depth checking in the flattener to avoid looping.

This implements (roughly) the plan put forward in comment:14:ticket:7788,
fixing #7788, #8550, #9554, #10139, and addressing concerns raised in #10079.
There are some regressions w.r.t. GHC 7.8, but only with pathological type
families (like F a = F a). This also (hopefully -- don't have a test case)
fixes #10158. Unsolved problems include #10184 and #10185, which are both
known deficiencies of the approach used here.

As part of this change, the plumbing around detecting infinite loops has
changed. Instead of -fcontext-stack and -ftype-function-depth, we now have
one combined -freduction-depth parameter. Setting it to 0 disbales the
check, which is now the recommended way to get (terminating) code to
typecheck in releases. (The number of reduction steps may well change between
minor GHC releases!)

This commit also introduces a new IntWithInf type in BasicTypes
that represents an integer+infinity. This type is used in a few
places throughout the code.

Tests in
  indexed-types/should_fail/T7788
  indexed-types/should_fail/T8550
  indexed-types/should_fail/T9554
  indexed-types/should_compile/T10079
  indexed-types/should_compile/T10139
  typecheck/should_compile/T10184  (expected broken)
  typecheck/should_compile/T10185  (expected broken)

This commit also changes performance testsuite numbers, for the better.

comment:4 Changed 3 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T9554

comment:5 Changed 23 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.