Opened 5 years ago

Last modified 2 years ago

#9729 new bug

GHCi accepts invalid programs when recompiling

Reported by: crockeea Owned by:
Priority: normal Milestone:
Component: GHCi Version: 8.0.1
Keywords: Cc: hvr, ezyang
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (7)

comment:1 Changed 5 years ago by crockeea

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.

comment:2 Changed 5 years ago by simonpj

Cc: ezyang added

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

comment:3 Changed 5 years ago by crockeea

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.

Last edited 5 years ago by crockeea (previous) (diff)

comment:4 Changed 5 years ago by simonpj

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

comment:5 Changed 5 years ago by simonpj

Edward is this fixed by your recent oprhan changes?

SImon

comment:6 Changed 3 years ago by ezyang

Version: 7.8.38.0.1

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!

comment:7 Changed 2 years ago by ezyang

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

Note: See TracTickets for help on using tickets.