[GHC] #12042: Infinite loop with type synonyms and hs-boot

[GHC]

#12042: Infinite loop with type synonyms and hs-boot
-------------------------------------+-------------------------------------
        Reporter:  ezyang            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  low               |            Milestone:
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |             Keywords:  hs-boot
      Resolution:                    |  backpack
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by ezyang:

@@ -80,3 +80,0 @@
-
- I take this bug as evidence that we should NOT attempt to knot-tie in this
- situation.

New description:

 This is a "known" bug, but the source code comment which mentioned this
 could happen didn't give a test case so I thought I'd supply one.

 {{{
 -- A.hs-boot
 module A where
 data S
 type R = S
 -- B.hs
 module B (module A, module B) where
 import {-# SOURCE #-} A
 type U = S
 -- A.hs
 module A where
 import qualified B
 type S = B.R
 type R = B.U
 }}}

 When I try to build `A.hs` in one-shot I infinite loop:

 {{{
 ezyang at sabre:~$ ghc-8.0 --make A.hs -fforce-recomp
 [1 of 3] Compiling A[boot]          ( A.hs-boot, A.o-boot )
 [2 of 3] Compiling B                ( B.hs, B.o )
 [3 of 3] Compiling A                ( A.hs, A.o )

 A.hs-boot:2:1: error:
     Type constructor ‘S’ has conflicting definitions in the module
     and its hs-boot file
     Main module: type S = R
     Boot file:   abstract S
 ezyang at sabre:~$ ghc-8.0 -c A.hs -fforce-recomp
 ^C
 }}}

 The problem is that `-c` properly knot ties `data S` in the boot file to
 the local type synonym (`--make` is unaffected due to #12035), and then we
 have a type synonym loop which GHC doesn't catch early enough.

 `TcTyDecls.hs` has a nice comment which suggests that this is a known bug:

 {{{
 Checking for class-decl loops is easy, because we don't allow class decls
 in interface files.

 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
 so we don't check for loops that involve them.  So we only look for
 synonym
 loops in the module being compiled.

 We check for type synonym and class cycles on the *source* code.
 Main reasons:

   a) Otherwise we'd need a special function to extract type-synonym tycons
      from a type, whereas we already have the free vars pinned on the decl

   b) If we checked for type synonym loops after building the TyCon, we
         can't do a hoistForAllTys on the type synonym rhs, (else we fall
 into
         a black hole) which seems unclean.  Apart from anything else, it'd
 mean
         that a type-synonym rhs could have for-alls to the right of an
 arrow,
         which means adding new cases to the validity checker

         Indeed, in general, checking for cycles beforehand means we need
 to
         be less careful about black holes through synonym cycles.

 The main disadvantage is that a cycle that goes via a type synonym in an
 .hi-boot file can lead the compiler into a loop, because it assumes that
 cycles
 only occur entirely within the source code of the module being compiled.
 But hi-boot files are trusted anyway, so this isn't much worse than (say)
 a kind error.
 }}}

 although the circumstances in this example are a little different.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12042#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler