GHCi accepts invalid programs when recompiling

Here's what's happening:

Module A imports module B. Module B contains a function with constraints that are required to compile module B. If I load module A in GHCi, I can remove some (required) constraints on the function in module B and GHCi will successfully reload module B.

My example uses the syntactic library. I attempted to recreate the situation I just described without syntactic, but I was unsuccessful.

Module A.hs:

module A where

import B
import Data.Syntactic.Sugar.BindingT ()

main = print "hello"

Module B.hs:

{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}

module B where

import Data.Syntactic

data Let x where
  Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          sup ~ Domain b, sup ~ Domain a,
          Internal (a -> b) ~ (Internal a -> Internal b), -- remove me
          Syntactic a, Syntactic b,
          Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) 
            (ASTF sup (Internal a) ->
              ASTF sup (Internal (a -> b)) ->
               ASTF sup (Internal b)))
      => a -> (a -> b) -> b
share = sugarSym Let

Here's a terminal transcript:

$ ghci A
[1 of 2] Compiling B    ( testsuite/B.hs, interpreted )
[2 of 2] Compiling A    ( testsuite/A.hs, interpreted )
Ok, modules loaded: A, B.
>
(Now remove the constraint from B and save. This *should* break module B)
> :r
[1 of 2] Compiling B    ( testsuite/B.hs, interpreted )
Ok, modules loaded: A, B.
> :q
$ ghci B
[1 of 2] Compiling B    ( testsuite/B.hs, interpreted )

testsuite/B.hs:21:9:
    Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

If I had to guess what's going on, it's that GHCi is remembering the instance that A imports from BindingT:

instance (...) => Syntactic (a -> b) where
  type Internal (a -> b) = Internal a -> Internal b

This instance implies the constraint that module B needs, however it should never be visible to module B. GHCi seems to be ignoring that and using the instance to recompile module B.

When compiling from scratch, module B is compiled first, so of course the instance (and therefore the constraint) are not visible.

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	GHCi
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	hvr
Operating system
Architecture

mentioned in issue #9717

changed weight to 5

added GHCi Tbug Trac import labels

I should have mentioned that following the same procedure with non-interactive GHC ("ghc A", then change B, then "ghc A" again) does detect the error in module B. So this problem appears to only affect GHCi.

I think your hypothesis is likely right. It's a long-standing deficiency in GHCi that it doesn't make instance declarations scope correctly, or (words) predictably. Edward Yang is thinking about ways to fix this.

Can you just be more explicit about what module B looks like after the edit? What, precisely, does "remove the constraint" mean?

Simon

By "remove the constraint", I mean comment that single line Internal (a -> b) ~ (Internal a -> Internal b) in the constraints for share. After the edit, module B is:

{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}

module B where

import Data.Syntactic

data Let x where
  Let :: Let (a :-> (a -> b) :-> Full b)

share :: (Let :<: sup,
          sup ~ Domain b, sup ~ Domain a,
          --Internal (a -> b) ~ (Internal a -> Internal b), -- remove me
          Syntactic a, Syntactic b,
          Syntactic (a -> b),
          SyntacticN (a -> (a -> b) -> b) 
            (ASTF sup (Internal a) ->
              ASTF sup (Internal (a -> b)) ->
               ASTF sup (Internal b)))
      => a -> (a -> b) -> b
share = sugarSym Let

The example is as minimal as I could make it. In particular, GHCi *does* detect the change to module B if I do not import BindingT in module A. This supports my hypothesis because the instance is never in scope. Also, GHC correctly throws an error when I remove any *other* constraint from share, so it is only failing to notice the constraint that is implied by the instance.

The problem is this.

• When compiling A we load up the interface file for Data.Syntactic.Sugar.BindingT, since A imports it. It includes an orphan instance declaration for the type family Internal.
• That populates the eps_fam_inst_env, globally across all packages, recording an instance for the type family Internal.
• Then when recompiling B we see the instance.

The solution, I think, is this:

• During instance lookup, for type families or classes, if the matched instance is an orphan, then check that the host module for the instance is transitively below the module being compiled.

We only need to do this check for orphan instance, because it's guaranteed true for non-orphans.

GHC already keeps a list of all the orphan modules transitively below the one being compiled, in the imp_orphs field of tcg_imports. So the check should be easy to do. That said, a ModuleSet would be better than a list, for fast membership checks.

Edward is already working on adding more info to the imp_orphs field: see Trac #9717. It might be better to combine the two.

Edward would you like to comment?

Simon

Edward is this fixed by your recent oprhan changes?

SImon

mentioned in issue #11577

mentioned in issue #13102

Unfortunately, I was able to reproduce with GHC 8.0.1, so I guess the visibility changes were not enough. Could it be that ~ instances are treated specially? Investigation necessary!

Trac metadata

Trac field	Value
Version	7.8.3 → 8.0.1

Actually, the orphan instance is a family instance, so this is just a case of #13102, I think!

added Pnormal label