Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,250
    • Issues 5,250
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 561
    • Merge requests 561
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #14435
Closed
Open
Issue created Nov 07, 2017 by Ryan Scott@RyanGlScottMaintainer

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

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
  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
Edited Mar 10, 2019 by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking