[GHC] #14396: Hs-boot woes during family instance consistency checks
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: -------------------------------------+------------------------------------- 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 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: 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 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: 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): 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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => hs-boot -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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 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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by inaki): * cc: inaki (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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 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.) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Changes (by ezyang): * status: new => patch * differential: => Phab:D4154 Comment: New patch up. Note that I haven't validated it yet, but it seems to pass the typecheck/driver tests. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"93b4820607aed1ab633e836084c5e39f5e631f87/ghc" 93b4820/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="93b4820607aed1ab633e836084c5e39f5e631f87" 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. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (by Edward Z. Yang <ezyang@…>): In [changeset:"6998772043a7f0b0360116eb5ffcbaa5630b21fb/ghc" 69987720/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6998772043a7f0b0360116eb5ffcbaa5630b21fb" 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 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: patch => closed * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (by juhpetersen): Anyone backported this patch to ghc-8.0.2? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14396: Hs-boot woes during family instance consistency checks -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: hs-boot 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: | -------------------------------------+------------------------------------- Comment (by bgamari): I'm afraid not and I believe it might be a rather tricky patch to backport. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14396#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC