Fix #15845 by defining etaExpandFamInstLHS and using it

Summary:
Both #9692 and #14179 were caused by GHC being careless
about using eta-reduced data family instance axioms. Each of those
tickets were fixed by manually whipping up some code to eta-expand
the axioms. The same sort of issue has now caused #15845, so I
figured it was high time to factor out the code that each of these
fixes have in common.

This patch introduces the `etaExpandFamInstLHS` function, which takes
a family instance's type variables, LHS types, and RHS type, and
returns type variables and LHS types that have been eta-expanded if
necessary, in the case of a data family instance. (If it's a type
family instance, `etaExpandFamInstLHS` just returns the supplied type
variables and LHS types unchanged).

Along the way, I noticed that many references to
`Note [Eta reduction for data families]` (in `FamInstEnv`) had
slightly bitrotted (they either referred to a somewhat different
name, or claimed that the Note lived in a different module), so
I took the liberty of cleaning those up.

Test Plan: make test TEST="T9692 T15845"

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15845

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

9 files changed, 86 insertions, 34 deletions

diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 9cef8753f9..31ac55fe5e 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1710,23 +1710,16 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
                                    (TH.TySynEqn th_tvs annot_th_lhs th_rhs)) }
 
       DataFamilyInst rep_tc ->
-        do { let rep_tvs = tyConTyVars rep_tc
-                 fam' = reifyName fam
-
-                   -- eta-expand lhs types, because sometimes data/newtype
-                   -- instances are eta-reduced; See Trac #9692
-                   -- See Note [Eta reduction for data family axioms]
-                   -- in TcInstDcls
-                 (_rep_tc, rep_tc_args) = splitTyConApp rhs
-                 etad_tyvars            = dropList rep_tc_args rep_tvs
-                 etad_tys               = mkTyVarTys etad_tyvars
-                 eta_expanded_tvs = mkTyVarTys fam_tvs `chkAppend` etad_tys
-                 eta_expanded_lhs = lhs `chkAppend` etad_tys
+        do { let -- eta-expand lhs types, because sometimes data/newtype
+                 -- instances are eta-reduced; See Trac #9692
+                 -- See Note [Eta reduction for data families] in FamInstEnv
+                 (ee_tvs, ee_lhs) = etaExpandFamInstLHS fam_tvs lhs rhs
+                 fam'             = reifyName fam
                  dataCons         = tyConDataCons rep_tc
                  isGadt           = isGadtSyntaxTyCon rep_tc
-           ; th_tvs <- reifyTyVarsToMaybe fam_tvs
-           ; cons <- mapM (reifyDataCon isGadt eta_expanded_tvs) dataCons
-           ; let types_only = filterOutInvisibleTypes fam_tc eta_expanded_lhs
+           ; th_tvs <- reifyTyVarsToMaybe ee_tvs
+           ; cons <- mapM (reifyDataCon isGadt (mkTyVarTys ee_tvs)) dataCons
+           ; let types_only = filterOutInvisibleTypes fam_tc ee_lhs
            ; th_tys <- reifyTypes types_only
            ; annot_th_tys <- zipWith3M annotThType is_poly_tvs types_only th_tys
            ; return $
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 919518c662..05b7536afd 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -211,20 +211,10 @@ ppr_co_ax_branch ppr_rhs
           = text "in" <+>
               quotes (ppr (nameModule name))
 
-        (ee_tvs, ee_lhs)
-          | Just (tycon, tc_args) <- splitTyConApp_maybe rhs
-          , isDataFamilyTyCon fam_tc
-          = -- Eta-expand LHS types, because sometimes data family instances
-            -- are eta-reduced.
-            -- See Note [Eta reduction for data family axioms] in TcInstDecls.
-            let tc_tvs           = tyConTyVars tycon
-                etad_tvs         = dropList tc_args tc_tvs
-                etad_tys         = mkTyVarTys etad_tvs
-                eta_expanded_tvs = tvs `chkAppend` etad_tvs
-                eta_expanded_lhs = lhs `chkAppend` etad_tys
-            in (eta_expanded_tvs, eta_expanded_lhs)
-          | otherwise
-          = (tvs, lhs)
+        -- Eta-expand LHS types, because sometimes data family instances
+        -- are eta-reduced.
+        -- See Note [Eta reduction for data families] in FamInstEnv.
+        (ee_tvs, ee_lhs) = etaExpandFamInstLHS tvs lhs rhs
 
 {-
 %************************************************************************
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index d149dbf1d0..6180bf12b2 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -7,6 +7,7 @@
 module FamInstEnv (
         FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
+        etaExpandFamInstLHS,
         pprFamInst, pprFamInsts,
         mkImportedFamInst,
 
@@ -212,6 +213,11 @@ For a FamInst with fi_flavour = DataFamilyInst rep_tc,
 But when fi_flavour = SynFamilyInst,
   - fi_tys has the exact arity of the family tycon
 
+There are certain situations (e.g., pretty-printing) where it is necessary to
+deal with eta-expanded data family instances. For these situations, the
+etaExpandFamInstLHS function exists as a convenient way to perform this eta
+expansion. (See #9692, #14179, and #15845 for examples of what can go wrong if
+etaExpandFamInstLHS isn't used).
 
 (See also Note [Newtype eta] in TyCon.  This is notionally separate
 and deals with the axiom connecting a newtype with its representation
@@ -555,7 +561,7 @@ irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
 Note [Compatibility of eta-reduced axioms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In newtype instances of data families we eta-reduce the axioms,
-See Note [Eta reduction for data family axioms] in TcInstDcls. This means that
+See Note [Eta reduction for data families] in FamInstEnv. This means that
 we sometimes need to test compatibility of two axioms that were eta-reduced to
 different degrees, e.g.:
 
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 7322a168ab..29f4b9a2d7 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -232,7 +232,7 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
         DataFamInstTyCon T [Int] ax_ti
 
 * The axiom ax_ti may be eta-reduced; see
-  Note [Eta reduction for data family axioms] in FamInstEnv
+  Note [Eta reduction for data families] in FamInstEnv
 
 * Data family instances may have a different arity than the data family.
   See Note [Arity of data families] in FamInstEnv
@@ -1010,8 +1010,8 @@ data AlgTyConFlav
                -- and R:T is the representation TyCon (ie this one)
                -- and a,b,c are the tyConTyVars of this TyCon
                --
-               -- BUT may be eta-reduced; see TcInstDcls
-               --     Note [Eta reduction for data family axioms]
+               -- BUT may be eta-reduced; see FamInstEnv
+               --     Note [Eta reduction for data families]
 
           -- Cached fields of the CoAxiom, but adjusted to
           -- use the tyConTyVars of this TyCon
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 5ab434f9ed..ba41388081 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -69,6 +69,8 @@ module Type (
 
         modifyJoinResTy, setJoinResTy,
 
+        etaExpandFamInstLHS,
+
         -- Analyzing types
         TyCoMapper(..), mapType, mapCoercion,
 
@@ -3049,6 +3051,43 @@ setJoinResTy :: Int  -- Number of binders to skip
 setJoinResTy ar new_res_ty ty
   = modifyJoinResTy ar (const new_res_ty) ty
 
+-- | Given a data or type family instance's type variables, left-hand side
+-- types, and right-hand side type, either:
+--
+-- * Return the eta-expanded type variables and left-hand types (if dealing
+--   with a data family instance). This function obtains the eta-reduced
+--   variables from the right-hand type, which is expected to be of the form
+--   @'mkTyConApp' rep_tc ('mkTyVarTys' tc_tvs)@.
+--
+-- * Just return the type variables and left-hand types (if dealing with a
+--   type family instance).
+--
+-- For an explanation of why data family instances need to have their
+-- left-hand sides eta-expanded, see
+-- @Note [Eta reduction for data families]@ in "FamInstEnv". Because the
+-- right-hand side is where the eta-reduced variables are obtained from, it
+-- is not returned from this function (as there is never a need to modify it).
+
+-- NB: In an ideal world, this would live in FamInstEnv, but this function
+-- is used in Coercion (which FamInstEnv imports), so doing so would lead to
+-- an import cycle.
+etaExpandFamInstLHS
+  :: [TyVar] -- ^ The type variables
+  -> [Type]  -- ^ The left-hand side types
+  -> Type    -- ^ The right-hand side type
+  -> ([TyVar], [Type])
+etaExpandFamInstLHS tvs lhs rhs
+  | Just (tycon, tc_args) <- splitTyConApp_maybe rhs
+  , isFamInstTyCon tycon
+  = let tc_tvs           = tyConTyVars tycon
+        etad_tvs         = dropList tc_args tc_tvs
+        etad_tys         = mkTyVarTys etad_tvs
+        eta_expanded_tvs = tvs `chkAppend` etad_tvs
+        eta_expanded_lhs = lhs `chkAppend` etad_tys
+    in (eta_expanded_tvs, eta_expanded_lhs)
+  | otherwise
+  = (tvs, lhs)
+
 {-
 %************************************************************************
 %*                                                                      *
diff --git a/testsuite/tests/th/T15845.hs b/testsuite/tests/th/T15845.hs
new file mode 100644
index 0000000000..b44808f25a
--- /dev/null
+++ b/testsuite/tests/th/T15845.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15845 where
+
+import Language.Haskell.TH
+import System.IO
+
+data family F1 a b
+data instance F1 [a] b = MkF1
+
+data family F2 a
+data instance F2 a = MkF2
+
+$(do i1 <- reify ''F1
+     i2 <- reify ''F2
+     runIO $ mapM_ (hPutStrLn stderr . pprint) [i1, i2]
+     pure [])
diff --git a/testsuite/tests/th/T15845.stderr b/testsuite/tests/th/T15845.stderr
new file mode 100644
index 0000000000..2b6a37e453
--- /dev/null
+++ b/testsuite/tests/th/T15845.stderr
@@ -0,0 +1,5 @@
+data family T15845.F1 (a_0 :: *) (b_1 :: *) :: *
+data instance forall (a_2 :: *) (b_3 :: *). T15845.F1 ([a_2]) b_3
+    = T15845.MkF1
+data family T15845.F2 (a_0 :: *) :: *
+data instance forall (a_1 :: *). T15845.F2 a_1 = T15845.MkF2
diff --git a/testsuite/tests/th/T9692.stderr b/testsuite/tests/th/T9692.stderr
index ffa55365d4..070e4d3005 100644
--- a/testsuite/tests/th/T9692.stderr
+++ b/testsuite/tests/th/T9692.stderr
@@ -1,2 +1,3 @@
 data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: *
-data instance T9692.F GHC.Types.Int (x_4 :: *) = T9692.FInt x_4
+data instance forall (x_4 :: *). T9692.F GHC.Types.Int (x_4 :: *)
+    = T9692.FInt x_4
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index 2481a2ab12..adf897081b 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -448,3 +448,4 @@ test('T15783', normal, multimod_compile,
 test('T15792', normal, compile, ['-v0 -dsuppress-uniques'])
 test('T15815', normal, multimod_compile,
     ['T15815B', '-v0 ' + config.ghc_th_way_flags])
+test('T15845', normal, compile, ['-v0 -dsuppress-uniques'])