Opened 5 months ago

Closed 5 months ago

#15380 closed bug (fixed)

Infinite typechecker loop in GHC 8.6

Reported by: RyanGlScott Owned by:
Priority: high Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType, TypeFamilies Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time performance bug Test Case: dependent/should_fail/T15380
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4974
Wiki Page:

Description

The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

class Generic a where
  type Rep a :: Type

class PGeneric a where
  type To a (x :: Rep a) :: a

type family MDefault (x :: a) :: a where
  MDefault x = To (M x)

class C a where
  type M (x :: a) :: a
  type M (x :: a) = MDefault x

In GHC 8.4.3, however this fails with a proper error:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:15:16: error:
    • Occurs check: cannot construct the infinite kind:
        a ~ Rep (M x) -> M x
    • In the type ‘To (M x)’
      In the type family declaration for ‘MDefault’
    • Type variable kinds: x :: a
   |
15 |   MDefault x = To (M x)
   |                ^^^^^^^^

Change History (8)

comment:1 Changed 5 months ago by RyanGlScott

Cc: goldfire added
Version: 8.4.38.5

This regression was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.).

comment:2 Changed 5 months ago by goldfire

Differential Rev(s): Phab:D4974
Status: newpatch

I really nailed this one. See the patch. :)

comment:3 Changed 5 months ago by goldfire

The patch now validates, but waiting for Simon's review before committing.

comment:4 Changed 5 months ago by simonpj

Richard and I discussed yesterday; he has a bit more to do and then will commmit.

comment:5 Changed 5 months ago by Richard Eisenberg <rae@…>

In f8618a9b/ghc:

Remove the type-checking knot.

Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.

This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.

The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.

Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!

NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.

There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.

Test case: dependent/should_fail/T15380

comment:6 Changed 5 months ago by goldfire

Status: patchmerge
Test Case: dependent/should_fail/T15380

Fixed now. Though this touches quite a few files, I don't think it should cause merging trouble. But it's not really critical.

comment:7 Changed 5 months ago by goldfire

Posted #15464 as the follow-up TH bug.

comment:8 Changed 5 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.