[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 (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------
Description changed by RyanGlScott:

Old description:

> 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]
> }}}

New description:

 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]
 instantiateTyN
 }}}

--

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