#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