Don't replace type family instances with the same LHS in GHCi (#7102)

This fixes the easy part of #7102 by removing the logic that lets the
user replace a type family instance with a new one with the same LHS.
As discussed on that ticket, this is unsound in general. Better to have
the user redefine the type family from scratch.

The example from comment:7 involving loading modules into ghci is not
fixed yet; it actually doesn't rely on the instances having the same LHS.
This commit adds an expect_broken test for that example as well.

Test Plan: T7102a for the fix; T7102 is the test not fixed yet

Reviewers: dfeuer, austin, bgamari, goldfire

Reviewed By: dfeuer

Subscribers: dfeuer, thomie

Differential Revision: https://phabricator.haskell.org/D2994

15 files changed, 84 insertions, 51 deletions

diff --git a/compiler/main/HscTypes.hs b/compiler/main/HscTypes.hs
index f44a261e76..d476fafb21 100644
--- a/compiler/main/HscTypes.hs
+++ b/compiler/main/HscTypes.hs
@@ -1583,7 +1583,9 @@ extendInteractiveContext ictxt new_tythings new_cls_insts new_fam_insts defaults
           , ic_tythings   = new_tythings ++ ic_tythings ictxt
           , ic_rn_gbl_env = ic_rn_gbl_env ictxt `icExtendGblRdrEnv` new_tythings
           , ic_instances  = ( new_cls_insts ++ old_cls_insts
-                            , new_fam_insts ++ old_fam_insts )
+                            , new_fam_insts ++ fam_insts )
+                            -- we don't shadow old family instances (#7102),
+                            -- so don't need to remove them here
           , ic_default    = defaults
           , ic_fix_env    = fix_env  -- See Note [Fixity declarations in GHCi]
           }
@@ -1593,7 +1595,6 @@ extendInteractiveContext ictxt new_tythings new_cls_insts new_fam_insts defaults
     -- See Note [Override identical instances in GHCi]
     (cls_insts, fam_insts) = ic_instances ictxt
     old_cls_insts = filterOut (\i -> any (identicalClsInstHead i) new_cls_insts) cls_insts
-    old_fam_insts = filterOut (\i -> any (identicalFamInstHead i) new_fam_insts) fam_insts
 
 extendInteractiveContextWithIds :: InteractiveContext -> [Id] -> InteractiveContext
 -- Just a specialised version
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index b9cf0af936..6a38f2f8d5 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -443,31 +443,26 @@ addLocalFamInst (home_fie, my_fis) fam_inst
         -- my_fies is just the ones from this module
   = do { traceTc "addLocalFamInst" (ppr fam_inst)
 
-       ; isGHCi <- getIsGHCi
-       ; mod <- getModule
-       ; traceTc "alfi" (ppr mod $$ ppr isGHCi)
+           -- Unlike the case of class instances, don't override existing
+           -- instances in GHCi; it's unsound. See #7102.
 
-           -- In GHCi, we *override* any identical instances
-           -- that are also defined in the interactive context
-           -- See Note [Override identical instances in GHCi] in HscTypes
-       ; let home_fie'
-               | isGHCi    = deleteFromFamInstEnv home_fie fam_inst
-               | otherwise = home_fie
+       ; mod <- getModule
+       ; traceTc "alfi" (ppr mod)
 
            -- Load imported instances, so that we report
            -- overlaps correctly
        ; eps <- getEps
-       ; let inst_envs  = (eps_fam_inst_env eps, home_fie')
-             home_fie'' = extendFamInstEnv home_fie fam_inst
+       ; let inst_envs = (eps_fam_inst_env eps, home_fie)
+             home_fie' = extendFamInstEnv home_fie fam_inst
 
            -- Check for conflicting instance decls and injectivity violations
        ; no_conflict    <- checkForConflicts            inst_envs fam_inst
        ; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
 
        ; if no_conflict && injectivity_ok then
-            return (home_fie'', fam_inst : my_fis)
+            return (home_fie', fam_inst : my_fis)
          else
-            return (home_fie,   my_fis) }
+            return (home_fie,  my_fis) }
 
 {-
 ************************************************************************
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index d23afad401..d4fc902be4 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -11,8 +11,8 @@ module FamInstEnv (
         mkImportedFamInst,
 
         FamInstEnvs, FamInstEnv, emptyFamInstEnv, emptyFamInstEnvs,
-        extendFamInstEnv, deleteFromFamInstEnv, extendFamInstEnvList,
-        identicalFamInstHead, famInstEnvElts, famInstEnvSize, familyInstances,
+        extendFamInstEnv, extendFamInstEnvList,
+        famInstEnvElts, famInstEnvSize, familyInstances,
 
         -- * CoAxioms
         mkCoAxBranch, mkBranchedCoAxiom, mkUnbranchedCoAxiom, mkSingleCoAxiom,
@@ -62,7 +62,6 @@ import SrcLoc
 import FastString
 import MonadUtils
 import Control.Monad
-import Data.Function ( on )
 import Data.List( mapAccumL, find )
 
 {-
@@ -425,33 +424,6 @@ extendFamInstEnv inst_env
   where
     add (FamIE items) _ = FamIE (ins_item:items)
 
-deleteFromFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
--- Used only for overriding in GHCi
-deleteFromFamInstEnv inst_env fam_inst@(FamInst {fi_fam = fam_nm})
- = adjustUDFM adjust inst_env fam_nm
- where
-   adjust :: FamilyInstEnv -> FamilyInstEnv
-   adjust (FamIE items)
-     = FamIE (filterOut (identicalFamInstHead fam_inst) items)
-
-identicalFamInstHead :: FamInst -> FamInst -> Bool
--- ^ True when the LHSs are identical
--- Used for overriding in GHCi
-identicalFamInstHead (FamInst { fi_axiom = ax1 }) (FamInst { fi_axiom = ax2 })
-  =  coAxiomTyCon ax1 == coAxiomTyCon ax2
-  && numBranches brs1 == numBranches brs2
-  && and ((zipWith identical_branch `on` fromBranches) brs1 brs2)
-  where
-    brs1 = coAxiomBranches ax1
-    brs2 = coAxiomBranches ax2
-
-    identical_branch br1 br2
-      =  isJust (tcMatchTys lhs1 lhs2)
-      && isJust (tcMatchTys lhs2 lhs1)
-      where
-        lhs1 = coAxBranchLHS br1
-        lhs2 = coAxBranchLHS br2
-
 {-
 ************************************************************************
 *                                                                      *
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index 1e53b6c32c..fa00b80244 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -655,11 +655,39 @@ The old, shadowed, version of ``T`` is displayed as
 ``main::Interactive.T`` by GHCi in an attempt to distinguish it from the
 new ``T``, which is displayed as simply ``T``.
 
-Class and type-family instance declarations are simply added to the list
-of available instances, with one exception. Since you might want to
-re-define one, a class or type-family instance *replaces* any earlier
-instance with an identical head or left hand side (respectively). (See
-:ref:`type-families`.)
+Class and type-family instance declarations are simply added to the
+list of available instances, with one exception. Since you might want
+to re-define one, a class instance *replaces* any earlier instance
+with an identical head. You aren't allowed to re-define a type family
+instance, since it might not be type safe to do so. Instead, re-define
+the whole type-family. (See :ref:`type-families`.) For example:
+
+.. code-block:: none
+
+    Prelude> type family T a b
+    Prelude> type instance T a b = a
+    Prelude> let uc :: a -> T a b; uc = id
+
+    Prelude> type instance T a b = b
+
+    <interactive>:3:15: error:
+        Conflicting family instance declarations:
+          T a b = a -- Defined at <interactive>:3:15
+          T a b = b -- Defined at <interactive>:5:15
+
+    -- Darn! We have to re-declare T.
+
+    Prelude> type family T a b
+    -- This is a brand-new T, unrelated to the old one
+    Prelude> type instance T a b = b
+    Prelude> uc 'a' :: Int
+
+    <interactive>:8:1: error:
+        • Couldn't match type ‘Char’ with ‘Int’
+          Expected type: Int
+            Actual type: Ghci1.T Char b0
+        • In the expression: uc 'a' :: Int
+          In an equation for ‘it’: it = uc 'a' :: Int
 
 .. _ghci-scope:
 
diff --git a/testsuite/tests/ghci/scripts/ghci046.script b/testsuite/tests/ghci/scripts/ghci046.script
index 28c5cde050..eee3683c07 100644
--- a/testsuite/tests/ghci/scripts/ghci046.script
+++ b/testsuite/tests/ghci/scripts/ghci046.script
@@ -1,4 +1,5 @@
 --Testing type families and their shadowing
+--(But type families no longer shadow, after #7102)
 :set -XTypeFamilies
 data HTrue
 data HFalse
diff --git a/testsuite/tests/ghci/scripts/ghci046.stderr b/testsuite/tests/ghci/scripts/ghci046.stderr
new file mode 100644
index 0000000000..e6a2bd0bfd
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/ghci046.stderr
@@ -0,0 +1,5 @@
+
+<interactive>:7:15: error:
+    Conflicting family instance declarations:
+      AND HTrue HTrue = HTrue -- Defined at <interactive>:7:15
+      AND HTrue HTrue = HFalse -- Defined at <interactive>:20:15
diff --git a/testsuite/tests/ghci/scripts/ghci046.stdout b/testsuite/tests/ghci/scripts/ghci046.stdout
index c4e7cf3fc7..921e453808 100644
--- a/testsuite/tests/ghci/scripts/ghci046.stdout
+++ b/testsuite/tests/ghci/scripts/ghci046.stdout
@@ -3,4 +3,4 @@ AND HTrue HTrue :: *
 AND (OR HFalse HTrue) (OR HTrue HFalse) :: *
 = HTrue
 t :: HTrue
-t :: HFalse
+t :: HTrue
diff --git a/testsuite/tests/indexed-types/should_fail/T7102.script b/testsuite/tests/indexed-types/should_fail/T7102.script
new file mode 100644
index 0000000000..6069cfd6c6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102.script
@@ -0,0 +1,5 @@
+:l T7102B T7102C
+:m +T7102C
+-- The empty T7102.stdout asserts that this :t fails
+-- (maybe because the earlier commands already did)
+:t to . from
diff --git a/testsuite/tests/indexed-types/should_fail/T7102.stdout b/testsuite/tests/indexed-types/should_fail/T7102.stdout
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102.stdout
diff --git a/testsuite/tests/indexed-types/should_fail/T7102A.hs b/testsuite/tests/indexed-types/should_fail/T7102A.hs
new file mode 100644
index 0000000000..86630bbf23
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102A.hs
@@ -0,0 +1,3 @@
+{-# LANGUAGE TypeFamilies #-}
+module T7102A where
+type family T a b
diff --git a/testsuite/tests/indexed-types/should_fail/T7102B.hs b/testsuite/tests/indexed-types/should_fail/T7102B.hs
new file mode 100644
index 0000000000..be2c17b962
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102B.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+module T7102B where
+import T7102A
+type instance T a b = a
+from :: a -> T a b
+from = id
diff --git a/testsuite/tests/indexed-types/should_fail/T7102C.hs b/testsuite/tests/indexed-types/should_fail/T7102C.hs
new file mode 100644
index 0000000000..b2cbe5f1b9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102C.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+module T7102C where
+import T7102A
+type instance T a b = b
+to :: T a b -> b
+to = id
diff --git a/testsuite/tests/indexed-types/should_fail/T7102a.script b/testsuite/tests/indexed-types/should_fail/T7102a.script
new file mode 100644
index 0000000000..40e1bada01
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102a.script
@@ -0,0 +1,4 @@
+:set -XTypeFamilies
+type family A a
+type instance A Int = ()
+type instance A Int = Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T7102a.stderr b/testsuite/tests/indexed-types/should_fail/T7102a.stderr
new file mode 100644
index 0000000000..8dd542391b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7102a.stderr
@@ -0,0 +1,5 @@
+
+<interactive>:3:15: error:
+    Conflicting family instance declarations:
+      A Int = () -- Defined at <interactive>:3:15
+      A Int = Bool -- Defined at <interactive>:4:15
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 4e3927797c..7f23c34fc5 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -128,3 +128,5 @@ test('T11450', normal, compile_fail, [''])
 test('T12041', normal, compile_fail, [''])
 test('T12522a', normal, compile_fail, [''])
 test('T12867', normal, compile_fail, [''])
+test('T7102', [ expect_broken(7102) ], ghci_script, ['T7102.script'])
+test('T7102a', normal, ghci_script, ['T7102a.script'])