[GHC] #13151: Make all never-exported IfaceDecls implicit

[GHC]

#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