GitLab

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