#13151: Make all never-exported IfaceDecls implicit -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: task | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: 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: | -------------------------------------+------------------------------------- Comment (by ezyang):

I suppose you could put all this in the instance decl. But would need to define the top-level Id $fEqList.

Yes, that's the idea. The upshot is that IfaceClsInst, which doesn't itself define any TyThings, can define an implicit TyThing, `$fEqList`. I agree that we still need a `TyThing` for `$fEqList`, but there isn't any reason `$fEqList` needs to live in `mi_decls`; we just have to make sure it gets to the type environment in the end. Today, if I'm looking for an `OccName` from an interface, it may either be defined directly by an entry in `mi_decls`, or it is one of the implicit things defined by one of the `IfaceDecl`. My suggestion is to expand this to also include implicit things defined by `IfaceClsInst`s.

I have not yet grokked what's hard about the status quo.

So, the problem is more pronounced for closed type families, so I'll do an example involving them. Suppose we have a signature that looks like this: {{{ signature A where type family F a where F a = Int }}} This will give us a type family, which refers to an axiom `TFCo:R:F` that specifies `F a ~ Int`. Furthermore, let's suppose that we're trying to match this against the following module: {{{ module A where type family F a where F a = Bool }}} When we typecheck the interface to make the TyThings for the type family we are going to compare, we need to need to resolve the Name `TFCo:R:F` from the hsig's interface to an actual Coercion. If we resolve `TFCo:R:F` to point to the *module*'s coercion, that's a disaster, because we never actually check that the top-level *coercions* match, we only check that the Coercion recorded in the type family (which we pointed at the module) matches. "Now," you might say, "why didn't you just have `TFCo:R:F` point to the hsig's version, then there's no problem." This is true, but in other cases, pointing to the module's versions of TyThings is very useful. Consider this other case: {{{ signature M where data T f :: T module M where type T = Int f :: Int }}} If the `T` in `f :: T` is not resolved to `type T = Int`, we will conclude that `f :: T` and `f :: Int` are incompatible, when they should be compatible! I'd quite like this to work: it's very important when implementing abstract data with type synonyms. The current implementation does a delicate tight-rope walk, of resolving names to the module version, except in the few cases where we need to resolve it to the hsig version. Highly delicate. Why does making the coercion *implicit* simplify things? With an implicit `TyThing`, we can avoid doing a lookup for the coercion at all; just use the implicit copy that was embedded. This means we sidestep the possible bug. We don't have to do this refactor: maybe the more complex interface typechecking for general users outweighs the simplification in the Backpack case. But I wanted to put this proposal out there. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13151#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler