Opened 9 months ago

Last modified 9 months ago

#16081 new bug

Clean up family instance consistency checking

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.3
Keywords: TypeFamilies Cc: ezyang
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown 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.

Change History (2)

comment:1 Changed 9 months ago by simonpj

Keywords: TypeFamilies added

comment:2 Changed 9 months ago by Simon Peyton Jones <simonpj@…>

In a57d5c4/ghc:

Fix treatment of hi-boot files and dfuns

Trac #16038 exposed the fact that TcRnDriver.checkHiBootIface
was creating a binding, in the module being compiled, for
   $fxBlah = $fBlah

 but $fxBlah was a /GlobalId/. But all bindings should be for
 /LocalIds/ else dependency analysis goes down the tubes.

* I added a CoreLint check that an occurrence of a GlobalId
  is not bound by an binding of a LocalId.  (There is already
  a binding-site check that no binding binds a GlobalId.)

* I refactored (and actually signficantly simplified) the
  tricky code for dfuns in checkHiBootIface to ensure that
  we get LocalIds for those boot-dfuns.

Alas, I then got "duplicate instance" messages when compiling
HsExpr. It turns out that this is a long-standing, but extremely
delicate, bug: even before this patch, if you compile HsExpr
with -ddump-tc-trace, you get "duplicate instance". Without
-ddump-tc-trace, it's OK.  What a mess!

The reason for the duplicate-instance is now explained in
Note [Loading your own hi-boot file] in LoadIface.  I fixed
it by a Gross Hack in LoadIface.loadInterface. This is at
least no worse than before.

But there should be a better way. I have opened #16081 for this.
Note: See TracTickets for help on using tickets.