#14435 closed bug (fixed)

GHC 8.2.1 regression: -ddump-tc-trace hangs forever

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by RyanGlScott)

Thanks to Christiaan Baaij for noticing this. Take this program:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Type.Equality
import GHC.TypeLits

type family Replicate (n :: Nat) (x :: a) :: [a] where
  Replicate 0 _ = '[]
  Replicate n x = x : Replicate (n - 1) x

replicateSucc :: (Replicate (k + 1) x) :~: (x : Replicate k x)
replicateSucc = Refl

Note that this program does not typecheck (nor should it). In GHC 8.0.2 and 8.2.1, if you compile this with no tracing flags, it'll give the error:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:16:17: error:
    • Couldn't match type ‘Replicate (k + 1) x’
                     with ‘x : Replicate k x’
      Expected type: Replicate (k + 1) x :~: (x : Replicate k x)
        Actual type: (x : Replicate k x) :~: (x : Replicate k x)
    • In the expression: Refl
      In an equation for ‘replicateSucc’: replicateSucc = Refl
    • Relevant bindings include
        replicateSucc :: Replicate (k + 1) x :~: (x : Replicate k x)
          (bound at Bug.hs:16:1)
16 | replicateSucc = Refl
   |                 ^^^^

Things become interesting when you compile this program with -ddump-tc-trace. In GHC 8.0.2, it'll trace some extra output and eventually reach the same error as above. In 8.2.1, however, the tracing hangs, causing compilation to never terminate! Here is the output right before it hangs:

lk1 :
tc_infer_args (invis) @a_11
tc_infer_args (vis)
  [anon] a_11
lk1 x_a1Dt
  tclvl 1
  k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
  arising from a type equality k0_a1GD[tau:1] ~ a0_a1GF[tau:1]
found filled tyvar k_a1GD[tau:1] :-> a0_a1GE[tau:1]
  tclvl 1
  * ~ *
  arising from a kind equality arising from
    a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
  tclvl 1
  'GHC.Types.LiftedRep ~ 'GHC.Types.LiftedRep
  arising from a kind equality arising from
    a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
u_tys yields no coercion
u_tys yields no coercion
writeMetaTyVar a_a1GE[tau:1] :: * := a0_a1GF[tau:1]
u_tys yields no coercion
tc_infer_args (vis)
  [anon] [a_11]
  Replicate (n_a1Ds - 1) x_a1Dt
lk1 Replicate
instantiating tybinders: @a_a1Dp := a0_a1GG[tau:1]

Change History (2)

comment:1 Changed 23 months ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 23 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

As it turns out, this has been fixed on GHC HEAD, by commit 791947db6db32ef7d4772a821a0823e558e3c05b (Refactor tcInferApps.), due to its removal of a call to ppr ty from a traceTc.

Note: See TracTickets for help on using tickets.