Opened 23 months ago

Closed 20 months ago

Last modified 20 months ago

#14396 closed bug (fixed)

Hs-boot woes during family instance consistency checks

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.2.1
Keywords: hs-boot Cc: inaki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4154
Wiki Page:

Description

Consider this set of modules (related to #13981 but not the same)

{-# LANGUAGE TypeFamilies #-}
module Fam where
  type family XListPat a

{-# LANGUAGE TypeFamilies #-}
module T1 where
  import Fam
  import {-# SOURCE #-} T( SyntaxExpr )
  type instance XListPat Int = SyntaxExpr

{-# LANGUAGE TypeFamilies #-}
module T2 where
  import Fam
  type instance XListPat Bool = Int

-- T.hs-boot
module T where
  data SyntaxExpr = S

-- T.hs
module T where
  import T1
  import T2
  data SyntaxExpr = S

Compiled with GHC 8.0, 8.2, and HEAD we get

ghc.exe: panic! (the 'impossible' happened)
  (GHC version 8.0.2 for x86_64-unknown-mingw32):
	tcIfaceGlobal (local): not found
  You are in a maze of twisty little passages, all alike.
  While forcing the thunk for TyThing SyntaxExpr
  which was lazily initialized by initIfaceTcRn,
  I tried to tie the knot, but I couldn't find SyntaxExpr
  in the current type environment.
  If you are developing GHC, please read Note [Tying the knot]
  and Note [Type-checking inside the knot].
  Consider rebuilding GHC with profiling for a better stack trace.
  Contents of current type environment: []

Reason:

  • After renaming, but before type checking, we try to do family-instance consistency checking in FamInst.checkFamInstConsistency

  • To do so we have to pull in the axioms from T1 and T2.
  • Then we poke on those axioms, to check consistency, we pull in both LHS and RHS of the type instances.
  • Alas that pulls on SyntaxExpr, which we have not yet typechecked.

I don't think it's enough to make lazier the loading of the RHS of the axiom, because I think checkFamInstConsistency ends up looking at the RHS too. See the call to compatibleBranches in lookupFamInstEnvConflicts.

This setup is actually used in Alan's wip/ttg-2017-10-13 branch for Trees That Grow. Here module T is HsExpr, T1 is HsPat. And indeed GHC 8.0 crashes when compiling this branch. SO it's becoming a real problem.

Generally I'm concerned that #13981 may also become more pressing; and #14080 is still open

Change History (14)

comment:1 Changed 23 months ago by goldfire

There's an off chance that considering #9562 may help to inform the solution here. That ticket is about a type system hole that opens up when you mix type families with hs-boot files -- quite unlike this ticket -- but it somehow may pay you back if you consider all these tickets together.

comment:2 Changed 23 months ago by ezyang

Going back to #11062

In this ticket, we decided to fix one particular version of the problem by *deferring* checking a boot-declared type family for conflicts until after we actually typechecked the type family. But as subsequent tickets demonstrated, it is not only the type family which can be defined too early: types referenced inside the LHS and RHS of the instance can also be referenced too early. So let's revisit the fix from before. Here is my proposal:

For every axiom, check it for consistency with the environment after all hs-boot types it mentions on the LHS or RHS (I am not sure if this has to be transitive) are finished being typechecked. The most expedient way to implement this is probably to extend FamInst to also record a list of "involved" Names, which we can key off of (we can't actually poke fi_tys or fi_rhs because they would trigger typechecking of the hs-boot type.)

comment:3 Changed 23 months ago by simonpj

Keywords: hs-boot added

comment:4 Changed 23 months ago by simonpj

Gah! This is ridiculously complicated. Surely there must be a better way.

In thinking about this I realised:

  • A very similar danger happens for ordinary data type decls:
        M.hs-boot    data S
    
        M1.hs        import {-# SOURCE #-} M
                     data D (a::S) = ...
    
        M.hs         import M1
                     data T a = MkT (D a)
                     data S = A | B
    
    The danger is that we'll kind-check the decl for T, suck in the interface decl for T1, and then find that S is not yet in the type envt.

But we fixed that (conservatively) in RnSource.addBootDeps; Note [Extra dependencies from .hs-boot files] in RnSource

  • Even within one module we have an open ticket about when to typecheck 'type instance' decls: #12088. It has a very similar flavour to the Edward's solution here.
  • Edward's solution defers the type family consistency check, but the interface-file instance is there in the family-instance environment all the time. e.g.
         M.hs-boot   data SyntaxExpr
    
         M1.hs       import {-# SOURCE #-} M
                     instance F Int = SyntaxExpr
    
         M.hs        import M1
                     data T = ...(F Int)...
                     data SyntaxExpr = SE
    
    I'm worried that an "earlier" decl, for T, might make use of that instance, which would again prematurely look for SyntaxExpr in the M's type environment, before it has been looked at.

Oh -- but maybe it's (just) ok: the fix in addBootDeps will ensure that SyntaxExpr is typechecked before T. But it's terribly delicate.

I did have one simplifying idea. Thought experiment:

  • When typechecking M, begin by loading M.hi-boot (which we already do) /and/ extend the type environment. So we'll add SyntaxExpr and W, in the above examples, to the type envt.
  • Do none of this addBootDeps stuff, nor deferring family instances. If we need W or SyntaxExpr before they've been encountered, we'll use the boot-versions.
  • So when compiling M we'll have places where we only have the boot TyCon instead of the real TyCon. Maybe that does not matter?
  • When we are all done, we'll spit out a M.hi file.
  • In --make mode we'll now re-typecheck the loop from the .hi files, building all the knots just as expected.

This is much much simpler. Would it work? Worth a a try?

comment:5 Changed 23 months ago by inaki

Cc: inaki added

comment:6 Changed 23 months ago by ezyang

I will give it an attempt :) (This is an obvious way how to do it, but we don't do it this way, which makes me wonder if there isn't some lurking hazard.)

comment:7 Changed 23 months ago by ezyang

Differential Rev(s): Phab:D4154
Status: newpatch

New patch up. Note that I haven't validated it yet, but it seems to pass the typecheck/driver tests.

comment:8 Changed 23 months ago by simonpj

That sounds good.

I suppose the worry is that, in Core, we might end up with something like

case x of
  A -> e1
  B -> e2

but find that x :: T and T is abstract (because it somehow came from the hs-boot file), whereas T is defined in this module with constructors A and B.

I can't see how this (or something like it) could happen; but I'm not sure how to convince ourselves that this can't.

comment:9 Changed 23 months ago by Ben Gamari <ben@…>

In 93b4820/ghc:

Revert "WIP on combining Step 1 and 3 of Trees That Grow"

This reverts commit 0ff152c9e633accca48815e26e59d1af1fe44ceb.

Sadly this broke when bootstrapping with 8.0.2 due to #14396.

Reverts haddock submodule.

comment:10 Changed 22 months ago by ezyang

I attempted to trigger the error case simonpj described, with the new patchset, by writing this T.hs instead:

-- T.hs
module T where
  import T1
  import T2
  data SyntaxExpr = S
f :: XListPat Int -> ()
f S = ()

But I didn't succeed. The idea is that type family consistency checking might have caused the family instance to force the thunk for SyntaxExpr early, so that the instance reduction will point to the wrong thing, but this does not seem to have happened.

comment:11 Changed 22 months ago by Edward Z. Yang <ezyang@…>

In 69987720/ghc:

Make use of boot TyThings during typechecking.

Summary:
Suppose that you are typechecking A.hs, which transitively imports,
via B.hs, A.hs-boot.  When we poke on B.hs and discover that it
has a reference to a type from A, what TyThing should we wire
it up with?  Clearly, if we have already typechecked A, we
should use the most up-to-date TyThing: the one we freshly
generated when we typechecked A.  But what if we haven't typechecked
it yet?

For the longest time, GHC adopted the policy that this was
*an error condition*; that you MUST NEVER poke on B.hs's reference
to a thing defined in A.hs until A.hs has gotten around to checking
this.  However, actually ensuring this is the case has proven
to be a bug farm.  The problem was especially poignant with
type family consistency checks, which eagerly happen before
any typechecking takes place.

This patch takes a different strategy: if we ever try to access
an entity from A which doesn't exist, we just fall back on the
definition of A from the hs-boot file.  This means that you may
end up with a mix of A.hs and A.hs-boot TyThings during the
course of typechecking.

Signed-off-by: Edward Z. Yang <ezyang@fb.com>

Test Plan: validate

Reviewers: simonpj, bgamari, austin, goldfire

Subscribers: thomie, rwbarton

GHC Trac Issues: #14396

Differential Revision: https://phabricator.haskell.org/D4154

comment:12 Changed 20 months ago by bgamari

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed

Hopefully fixed with comment:11.

Last edited 20 months ago by bgamari (previous) (diff)

comment:13 Changed 20 months ago by juhpetersen

Anyone backported this patch to ghc-8.2.2?

Last edited 20 months ago by juhpetersen (previous) (diff)

comment:14 Changed 20 months ago by bgamari

I'm afraid not and I believe it might be a rather tricky patch to backport.

Note: See TracTickets for help on using tickets.