Type checking fails to terminate in GHC 9.2, 9.8, 9.10, and 9.12

Summary

Compilation of the attached code seems to result in an infinite loop in GHC 9.2, 9.8, 9.10, and 9.12, whereas GHC 9.4 and 9.6 compile it successfully without any issues. The issue appears to occur during the type-checking phase because invoking GHC with -dshow-passes stalls after displaying *** Renamer/typechecker [Main].

The code to reproduce this issue is available at https://github.com/kztk-m/issue_in_ghc/blob/d99a7bfc6b422d762cfdc9fd2c3ebe5206488fa2/app/Main.hs. For convenience, the same code is also attached to this issue: Main.hs

With GHC 9.2, 9.8, 9.10, and 9.12. The following line causes the type checker to go into an infinite loop (or take an unexpectedly long time).

f :: (EnvI Sem a -> EnvI Sem b) -> EnvI Sem (a -> b)
f = lifts (ECons (liftOfLength (LS LZ)) ENil)

Here, lifts has the following type:

lifts :: Env DimSimple ss -> FuncU sem ss r

The following are (seemingly) relevant type families and type classes. They are pretty complex, but I failed to reproduce the issue with my further simplification attempt (see below).

type family Func sem as r where
  Func sem '[] r       = r
  Func sem (a ': as) r = sem a -> Func sem as r


type family FuncU (sem :: [k] -> k -> Type) (ss :: [Sig2 k])
                  (r :: k) = res | res -> sem r where
  FuncU sem '[] r = EnvI sem r
  FuncU sem ((as ':~> a) ': ss) r = Func (EnvI sem) as (EnvI sem a)
                                    -> FuncU sem ss r

data Env (f :: k -> Type) (as :: [k]) where
  ENil  :: Env f '[]
  ECons :: f a -> Env f as -> Env f (a ': as)

data Sig2 k = [k] :~> k

data DimSimple (s :: Sig2 k) where
  DimSimple :: OfLength as -> DimSimple (as ':~> a)

data OfLength as where
  LZ :: OfLength '[]
  LS :: OfLength as -> OfLength (a ': as)

class LiftOfLength f as t | t -> as where
  liftOfLength :: OfLength as -> f t

instance t ~ (as ':~> a) => LiftOfLength DimSimple as t where
  liftOfLength = undefined

data EnvI (sem :: [k] -> k -> Type) (a :: k) 

Interestingly, the nontermination issue is fragile as the following variations did not cause the issue (in GHC 9.8.4).

• f = undefined $ lifts (ECons (liftOfLength (LS LZ)) ENil)
• f = let h = lifts (ECons (liftOfLength (LS LZ)) ENil) in h
• f = h where h = lifts (ECons (liftOfLength (LS LZ)) ENil)
• f = lifts (ECons (DimSimple (LS LZ)) ENil) (replaced the class method liftOfLength with its implementation)
• f = lifts d where {d :: Env DimSimple '[ '[a] :~> b ]; d = (ECons (liftOfLength (LS LZ)) ENil) }
• f = lift (liftOfLength (LS LZ)) (replaced the type family FuncU with its specialization to the singleton FuncS)
• f = (lifts :: Env DimSimple ss -> FuncU Sem ss r) (ECons (liftOfLength (LS LZ)) ENil)
• f without its signature

In contrast, there is no issue with the code with GHC 9.4 and 9.6. The compilation succeeds in around a second on my machine.

Steps to reproduce

1. Run ghc Main.hs using the attached Main.hs.

or

1. Clone the repository https://github.com/kztk-m/issue_in_ghc

   git clone https://github.com/kztk-m/issue_in_ghc.git

2. Execute cabal build

Expected behavior

Compilation should complete within a few seconds (as with GHC 9.4 and 9.6) or fail with appropriate error messages.

Environment

• GHC version used: 9.2.5, 9.8.4, 9.4.8, 9.6.6, 9.10.1, 9.12.1

Optional:

• Operating System: macOS Sonoma 15.1.1
• System Architecture: Apple M1 Mac

The result of GitHub Action suggests that this is not a Mac-specific issue, and we also have the issue with GHC 9.0.