[GHC] #7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module

[GHC]

#7672: boot file entities are sometimes invisible and are not (semantically)
unified with corresponding entities in implementing module
-----------------------------+----------------------------------------------
Reporter:  skilpat           |          Owner:                                                                     
    Type:  bug               |         Status:  new                                                                
Priority:  normal            |      Component:  Compiler (Type checker)                                            
 Version:  7.4.2             |       Keywords:  recursive modules, boot files, double vision, double vision problem
      Os:  Unknown/Multiple  |   Architecture:  x86_64 (amd64)                                                     
 Failure:  None/Unknown      |      Blockedby:                                                                     
Blocking:                    |        Related:                                                                     
-----------------------------+----------------------------------------------
 In a recursive module (i.e. a module that transitively imports itself),
 the unique "Name" of an entity E declared in this module's boot file
 should be precisely the same as that of the corresponding E defined in the
 module. Right now GHC appears to treat them as separate entities. (In the
 module systems literature, this problem has been identified as the "double
 vision problem" [1, Ch 5] and in general has caused problems with
 implementations of recursive modules. Derek Dreyer and his coauthors have
 proposed a number of solutions [2], and so have Im et al. more recently in
 the context of OCaml [3].)

 With that being said, the ''immediate'' problem here seems to be that GHC
 does not actually allow, in the implementing module, the import of its
 boot file's entities.

 There are a couple related errors I can identify with, huzzah!, very small
 example programs. The crux of the example is that the module A defines a
 data type T which is essentially the typical Nat data type -- except that
 the recursive type reference in the successor constructor refers to the
 "forward declaration's" view of the type (in the boot file) rather than
 the local view of that data type T.

 This first example shows that the boot file import is not actually making
 available the entities it declares:
 {{{
 module A where
   data T
 }}}
 {{{
 module A where
   import {-# SOURCE #-} qualified A as Decl(T)
   data T = Z | S Decl.T
 }}}
 The Decl.T reference should have the exact same identity as the locally
 defined T reference; after tying the module knot, this data type should be
 the same as if we had defined it with a T instead of Decl.T. However, the
 entity name T does not even appear to be gotten from the import of the
 boot file:
 {{{
 A.hs:3:18: Not in scope: type constructor or class `Decl.T'
 }}}
 In an earlier version of GHC I tested, 6.12.1, the error message lies on
 the import statement:
 {{{
 A.hs:2:44: Module `A' (hi-boot interface) does not export `T'
 }}}

 In the next example, with the same boot file, we see that the mechanism
 that checks whether the implementation matches the boot file fails to see
 the two "views" of T as the same. (Note that I changed the definition of T
 here to make the previous error go away.)
 {{{
 module A(Decl.T(..)) where
   import {-# SOURCE #-} qualified A as Decl(T)
   data T = Z | S T
 }}}
 Since Decl.T should point to the same entity as T, the export statement
 should have the same effect as if it were instead "(T(..))". However, GHC
 again cannot make sense of the reference "Decl.T" and then complains that
 the boot file's T is not provided in the implementation:
 {{{
 A.hs:1:10: Not in scope: type constructor or class `Decl.T'

 <no location info>:
     T is exported by the hs-boot file, but not exported by the module
 }}}
 (Making the export list empty shows this second error message only.)

 Altering this second example by omitting the alias on the import, and by
 changing the T reference in the type's definition to A.T, results in a
 well-typed module:
 {{{
 module A(A.T(..)) where
   import {-# SOURCE #-} qualified A(T)
   data T = Z | S A.T
 }}}

 A final example shows that, in a module that is ''not'' the implementing
 module, entities defined in the boot file are imported as one would
 expect! In the following example, we insert a module B, in between A's
 boot file and A's implementation, which merely passes along the boot
 file's view of T.
 {{{
 module A where
   data T
 }}}
 {{{
 module B(Decl.T(..)) where
   import {-# SOURCE #-} qualified A as Decl(T)
   data U = U Decl.T
 }}}
 {{{
 module A(T(..)) where
   import qualified B(T)
   data T = Z | S B.T
 }}}
 The error message here, again, lies in the reference B.T in A's
 implementation:
 {{{
 A.hs:3:18:
     Not in scope: type constructor or class `B.T'
     Perhaps you meant `A.T' (line 3)
 }}}
 Notice, however, that the reference to Decl.T in the B module is perfectly
 well-formed.

 I suspect that the general problem lies with double vision, and that the
 more immediate problem--whereby imports of boot file entities from their
 implementing modules fail--is merely the manifestation of that.

 In the above, wherever I have suggested an intended semantics, I refer
 primarily to the state of the art in recursive modules systems. A perhaps
 more pressing justification, however, is that both the Haskell language
 report and Diatchki et al.'s specification of the module system [4] (seem
 to) corroborate that intended semantics.

 Your friend in the recursive module swamp,[[BR]]
 Scott Kilpatrick

 ----

 References

 [1] Derek Dreyer. ''[http://www.mpi-sws.org/~dreyer/thesis/main.pdf
 Understanding and Evolving the ML Module System]'', PhD thesis,
 2005.[[BR]]
 [2] Derek Dreyer. ''[http://www.mpi-
 sws.org/~dreyer/courses/modules/dreyer07.pdf A Type System for Recursive
 Modules]'', ICFP 2007.[[BR]]
 [3] Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park.
 ''[http://dl.acm.org/citation.cfm?doid=2048066.2048141 A syntactic type
 system for recursive modules]'', OOPSLA 2011.[[BR]]
 [4] Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren.
 ''[http://web.cecs.pdx.edu/~mpj/pubs/hsmods.html A formal specification of
 the Haskell 98 module system]'', Haskell 2002.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7672>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler