[GHC] #14435: GHC 8.2.1 regression: -ddump-tc-trace hangs forever

[GHC]

#14435: GHC 8.2.1 regression: -ddump-tc-trace hangs forever
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  performance bug
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Thanks to Christiaan Baaij for noticing this. Take this program:

 {{{#!hs
 {-# 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
   x_a1Dt
 lk1 x_a1Dt
 u_tys
   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]
 u_tys
   tclvl 1
   * ~ *
   arising from a kind equality arising from
     a0_a1GE[tau:1] ~ a0_a1GF[tau:1]
 u_tys
   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
 checkExpectedKind
   k0_a1GD[tau:1]
   a0_a1GF[tau:1]
   <a0_a1GF[tau:1]>_N
 tc_infer_args (vis)
   [anon] [a_11]
   Replicate (n_a1Ds - 1) x_a1Dt
 lk1 Replicate
 instantiating tybinders: @a_a1Dp := a0_a1GG[tau:1]
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14435>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler