# 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 |