Opened 2 years ago

Last modified 6 days ago

#7672 new bug

boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing module

Reported by: skilpat Owned by: ezyang
Priority: normal Milestone: 7.12.1
Component: Compiler (Type checker) Version: 7.4.2
Keywords: backpack Cc: pho@…
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking: #10336
Related Tickets: Differential Revisions:

Description

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,
Scott Kilpatrick


References

[1] Derek Dreyer. Understanding and Evolving the ML Module System, PhD thesis, 2005.
[2] Derek Dreyer. A Type System for Recursive Modules, ICFP 2007.
[3] Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park. A syntactic type system for recursive modules, OOPSLA 2011.
[4] Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren. A formal specification of the Haskell 98 module system, Haskell 2002.

Change History (11)

comment:1 Changed 2 years ago by PHO

  • Cc pho@… added

comment:2 Changed 2 years ago by skilpat

  • Operating System changed from Unknown/Multiple to Linux
  • Type of failure changed from None/Unknown to GHC rejects valid program

comment:3 Changed 2 years ago by skilpat

I must scale back my assessment of the problem somewhat: double vision is indeed handled, to some extent, by GHC. In particular, a view of a type from a boot file is treated as an equivalent type to a view of that type from the implementation. That's good! But you still cannot syntactically refer to both views in the same program. That's less good.

As a slight variation to my example with three modules, we make B expose a function that mentions (the boot file's view of) T. Then in the A implementation, we check that this function may be successfully applied to a value of (the local view of) type T. Indeed, GHC accepts all this!

module A where
  data T
module B(Decl.T, f) where
  import {-# SOURCE #-} qualified A as Decl
  f :: Decl.T -> Bool
  f _ = True
module A where
  import qualified B
  data T = Z | S T
  x = B.f Z

In the A implementation I'm not ever mentioning the boot file view of T, B.T. If you try to do so, then GHC rejects the program with the same error messages as mentioned in the original report. That is, the following variation on A fails

module A where
  import qualified B
  data T = Z | S B.T
  x = B.f Z :: B.T

with two independent errors, one for each reference to B.T:

A.hs:3:18:
    Not in scope: type constructor or class `B.T'
    Perhaps you meant `A.T' (line 3)

A.hs:4:16:
    Not in scope: type constructor or class `B.T'
    Perhaps you meant `A.T' (line 3)

In light of this example, I retract my statement that GHC fails to solve the double vision problem! It's unclear, though, to what extent it does so, as there's still some amount of wackiness.

comment:4 Changed 2 years ago by igloo

  • difficulty set to Unknown
  • Milestone set to 7.8.1

Thanks for the report.

comment:5 Changed 12 months ago by thoughtpolice

  • Milestone changed from 7.8.3 to 7.10.1

Moving to 7.10.1

comment:6 Changed 10 months ago by ezyang

  • Keywords backpack added; recursive modules boot files double vision double vision problem removed

comment:7 Changed 4 months ago by thoughtpolice

  • Milestone changed from 7.10.1 to 7.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:8 Changed 7 days ago by ezyang

The reason this occurs is when we process imports in rnImportDecl, we filter out any identifiers which come from a self-boot:

    let gbl_env = mkGlobalRdrEnv (filterOut from_this_mod gres)

So these identifiers never get added to the GlobalRdrEnv, and thus aren't brought into scope.

I don't know what happens if you remove that filterOut. It comes from some very old code.

comment:9 Changed 7 days ago by simonpj

  • Owner set to ezyang

I agree. Just remove it and see. It looks outright wrong to me.

Simon

comment:10 Changed 7 days ago by ezyang

  • Blocking 10336 added

comment:11 Changed 6 days ago by ezyang

Removing the filterOut does not work. (insert more info here)

Note: See TracTickets for help on using tickets.