[GHC] #9729: GHCi accepts invalid programs when recompiling

[GHC]

#9729: GHCi accepts invalid programs when recompiling
-------------------------------------+-------------------------------------
       Reporter:  crockeea           |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  GHCi               |                 Version:  7.8.3
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:  GHC
     Blocked By:                     |  accepts invalid program
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 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 [https://hackage.haskell.org/package/syntactic
 syntactic] library. I attempted to recreate the situation I just described
 without syntactic, but I was unsuccessful.

 Module A.hs:
 {{{
 #!haskell
 module A where

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

 main = print "hello"
 }}}

 Module B.hs:

 {{{
 #!haskell
 {-# 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9729>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler