[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

#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

#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