[GHC] #16081: Clean up family instance consistency checking

21 Dec 2018

      #16081: Clean up family instance consistency checking
-------------------------------------+-------------------------------------
           Reporter:  simonpj        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 There is a big mess concerning consistency checking for family instances.
 It's described in `Note [The type family instance consistency story]` in
 `FamInst`, which is reproduced below.

 Note in particular the "four subtle points that have not been addressed
 yet".  The fourth one bit me today, and forced me to introduce a new hack
 into `loadIface`, described in `Note [Loading your own hi-boot file]` in
 `LoadIface`.

 Somehow we should be able to do better!
 {{{
 {- Note [The type family instance consistency story]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 To preserve type safety we must ensure that for any given module, all
 the type family instances used either in that module or in any module
 it directly or indirectly imports are consistent. For example, consider

   module F where
     type family F a

   module A where
     import F( F )
     type instance F Int = Bool
     f :: F Int -> Bool
     f x = x

   module B where
     import F( F )
     type instance F Int = Char
     g :: Char -> F Int
     g x = x

   module Bad where
     import A( f )
     import B( g )
     bad :: Char -> Int
     bad c = f (g c)

 Even though module Bad never mentions the type family F at all, by
 combining the functions f and g that were type checked in contradictory
 type family instance environments, the function bad is able to coerce
 from one type to another. So when we type check Bad we must verify that
 the type family instances defined in module A are consistent with those
 defined in module B.

 How do we ensure that we maintain the necessary consistency?

 * Call a module which defines at least one type family instance a
   "family instance module". This flag `mi_finsts` is recorded in the
   interface file.

 * For every module we calculate the set of all of its direct and
   indirect dependencies that are family instance modules. This list
   `dep_finsts` is also recorded in the interface file so we can compute
   this list for a module from the lists for its direct dependencies.

 * When type checking a module M we check consistency of all the type
   family instances that are either provided by its `dep_finsts` or
   defined in the module M itself. This is a pairwise check, i.e., for
   every pair of instances we must check that they are consistent.

   - For family instances coming from `dep_finsts`, this is checked in
     checkFamInstConsistency, called from tcRnImports. See Note
     [Checking family instance consistency] for details on this check
     (and in particular how we avoid having to do all these checks for
     every module we compile).

   - That leaves checking the family instances defined in M itself
     against instances defined in either M or its `dep_finsts`. This is
     checked in `tcExtendLocalFamInstEnv'.

 There are four subtle points in this scheme which have not been
 addressed yet.

 * We have checked consistency of the family instances *defined* by M
   or its imports, but this is not by definition the same thing as the
   family instances *used* by M or its imports.  Specifically, we need to
   ensure when we use a type family instance while compiling M that this
   instance was really defined from either M or one of its imports,
   rather than being an instance that we happened to know about from
   reading an interface file in the course of compiling an unrelated
   module. Otherwise, we'll end up with no record of the fact that M
   depends on this family instance and type safety will be compromised.
   See #13102.

 * It can also happen that M uses a function defined in another module
   which is not transitively imported by M. Examples include the
   desugaring of various overloaded constructs, and references inserted
   by Template Haskell splices. If that function's definition makes use
   of type family instances which are not checked against those visible
   from M, type safety can again be compromised. See #13251.

 * When a module C imports a boot module B.hs-boot, we check that C's
   type family instances are compatible with those visible from
   B.hs-boot. However, C will eventually be linked against a different
   module B.hs, which might define additional type family instances which
   are inconsistent with C's. This can also lead to loss of type safety.
   See #9562.

 * The call to checkFamConsistency for imported functions occurs very
   early (in tcRnImports) and that causes problems if the imported
   instances use type declared in the module being compiled.
   See Note [Loading your own hi-boot file] in LoadIface.
 -}
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16081
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler