#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