#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I managed to break type family consistency in 8.0.1 using `ghc -c` alone, but apparently it was in some way that fooled the recompilation checker and it can't be reproduced from a clean build. So I don't know how I did it. In any case, it seems more logical for the type family instances in `A` to be checked against `B` while compiling `A`, rather than forcing every importer of `A` to do it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I managed to write `unsafeCoerce` in 8.0.1 without involving recompilation tricks. Compile these modules in order with `ghc -c -XTypeFamilies -fforce-recomp` (then you can do a final link with `ghc -o Main Main.hs -XTypeFamilies`): {{{#!hs module A where type family A a }}} {{{#!hs module B (A, X) where import A data X type instance A (X, b) = () }}} {{{#!hs {-# LANGUAGE RankNTypes #-} module C (x) where import Data.Proxy import B x :: Proxy b -> (forall t. Proxy t -> Bool -> A (t, b)) -> (Bool -> ()) x _ f = f (undefined :: Proxy X) }}} {{{#!hs module Main where import Data.Proxy import A import C data Y type instance A (a, Y) = Bool y :: Proxy a -> Bool -> A (a, Y) y _ = id z :: Bool -> () z = x (undefined :: Proxy Y) y main = print (z True) }}} `Main` has been rigged to not directly mention any names defined in `B`, by creating the intermediate module `C`. When `Main` is compiled the interface file for `B` is not read at all! There is a kind of off-by-one error in the check. The logic in the Note `[Checking family instance consistency]` correctly takes into account the fact that we do not check consistency of family instances in a module with those in its `dep_finsts`, and so if you try to import `Main` in another module (even one that is otherwise empty) GHC will report the overlap. But that still leaves a window of one module in which the overlap can be exploited. Even if not for this example I agree with

But regardless, I think it'd be better and more consistent to eagerly check consistency of all the new family instances in A with all those in modules it imports. Then instance lookup should never find more than one match.

I think it's even more efficient overall, since we currently do those checks in the importers of `A` instead, which usually will be at least one module. If we do them while compiling `A` then the optimization that this ticket was originally about will be sound and we can avoid the checks in the importers. I also figured out what my example involving recompilation was, I'll file a separate ticket for that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):

When Main is compiled the interface file for B is not read at all!

Ah, that is the bit I was missing! (It's not read, because nobody mentions `X`.) If B.hi was read we would (I hope) get an overlap error when solving `(A (a,y))`. Well done! In fixing this, do give a careful account of the invariants etc. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:5 simonpj]:

Actually there is ''some'' justification for the status quo.

... except that, regardless of Reid's excellent example in comment:6, having `F Int = Bool` and `F Int = Char` in scope means that we can write a proof of `Bool ~ Char` in Core. Continuing the status quo means that Core Lint is much less useful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): I think so. My plan is to proceed as in 608cad595c033ba89e757c8f61a9b791a7085367 though of course it still needs explanation and tests. The new code is basically copied from `tcRnImports` where it loads orphan modules. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13092: family instance consistency checks are too pessimistic -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: rwbarton Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2992 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I think the Phab is fine, but here's a possible thought for improvement to `checkFamInstConsistency`. Currently it does an all-pairs enumeration, and filters out pairs that are already known consistent. That sounds like enumerating a large set and then filtering it. What about this. Take just two imported modules A and B, with `dep_finsts` dA and dB resp. So we know that `A + dA` is consistent and `B + dB` is consistent. What extra parirwise checks do we need to make to ensure that `uAB` is consistent, where {{{ uAB = A + dA + B + dB }}} (I'm using `+` for set union.) Well, define {{{ iAB = (A + dA) `intersect` (B + dB) }}} so that `iAB` is the intersection; certainly it is consistent all of `uAB`. Now define {{{ xA = (A + dA) - iAB xB = (B + dB) - iAB }}} If we check all the pairs with one from `xA` and one from `xB` we are done. So check those and form the union `uAB`. Now continue by adding in one more module, and keep doing that a time. The bigger the intersection the better. I'm not certain that is better, but it smells better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13092#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler