Fix #15852 by eta expanding data family instance RHSes, too

When I defined `etaExpandFamInstLHS`, I blatantly forgot
to eta expand the RHSes of data family instances. (Actually, I
claimed that they didn't //need// to be eta expanded. I'm not sure
what I was thinking.)

This fixes the issue by changing `etaExpandFamInstLHS` to
`etaExpandFamInst` and, well, making it actually eta expand the RHS.

Test Plan: make test TEST=T15852

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15852

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

14 files changed, 115 insertions, 47 deletions

diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs
index c3ee937baa..3032c0ccd8 100644
--- a/compiler/basicTypes/OccName.hs
+++ b/compiler/basicTypes/OccName.hs
@@ -859,6 +859,8 @@ avoidClashesOccEnv env occs = go env emptyUFM occs
 tidyOccName :: TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
 tidyOccName env occ@(OccName occ_sp fs)
   | not (fs `elemUFM` env)
+    && (fs /= fsLit "_")
+        -- See Note [Always number wildcard types when tidying]
   = (addToUFM env fs 1, occ)   -- Desired OccName is free
   | otherwise
   = case lookupUFM env base1 of
@@ -886,6 +888,34 @@ tidyOccName env occ@(OccName occ_sp fs)
                      -- See Note [TidyOccEnv]
 
 {-
+Note [Always number wildcard types when tidying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following example (from the DataFamilyInstanceLHS test case):
+
+  data family Sing (a :: k)
+  data instance Sing (_ :: MyKind) where
+      SingA :: Sing A
+      SingB :: Sing B
+
+If we're not careful during tidying, then when this program is compiled with
+-ddump-types, we'll get the following information:
+
+  COERCION AXIOMS
+    axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
+      Sing _ = DataFamilyInstanceLHS.R:SingMyKind_ _
+
+Yikes! We shouldn't have a wildcard type appearing on the RHS like that. To
+avoid this issue, during tidying, we always opt to add a numeric suffix to
+types that are simply `_`. That way, you instead end up with:
+
+  COERCION AXIOMS
+    axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
+      Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
+
+Which is at least legal syntax.
+-}
+
+{-
 ************************************************************************
 *                                                                      *
                 Binary instance
diff --git a/compiler/iface/ToIface.hs-boot b/compiler/iface/ToIface.hs-boot
index e5f57ff9a3..6e2fc66ee6 100644
--- a/compiler/iface/ToIface.hs-boot
+++ b/compiler/iface/ToIface.hs-boot
@@ -4,6 +4,7 @@ import {-# SOURCE #-} TyCoRep
 import {-# SOURCE #-} IfaceType( IfaceType, IfaceTyCon, IfaceForAllBndr
                                , IfaceCoercion, IfaceTyLit, IfaceAppArgs )
 import Var ( TyCoVarBinder )
+import VarEnv ( TidyEnv )
 import TyCon ( TyCon )
 import VarSet( VarSet )
 
@@ -14,3 +15,4 @@ toIfaceForAllBndr :: TyCoVarBinder -> IfaceForAllBndr
 toIfaceTyCon :: TyCon -> IfaceTyCon
 toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
 toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion
+tidyToIfaceTcArgs :: TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 5fd91c6b3b..b3cf4d97c5 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1713,10 +1713,10 @@ reifyFamilyInstance is_poly_tvs inst@(FamInst { fi_flavor = flavor
         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
+                 (ee_tvs, ee_lhs, _) = etaExpandFamInst fam_tvs lhs rhs
+                 fam'                = reifyName fam
+                 dataCons            = tyConDataCons rep_tc
+                 isGadt              = isGadtSyntaxTyCon rep_tc
            ; th_tvs <- reifyTyVarsToMaybe ee_tvs
            ; cons <- mapM (reifyDataCon isGadt (mkTyVarTys ee_tvs)) dataCons
            ; let types_only = filterOutInvisibleTypes fam_tc ee_lhs
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 05b7536afd..529f90a964 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -109,8 +109,11 @@ module Coercion (
 
 #include "HsVersions.h"
 
+import {-# SOURCE #-} ToIface (toIfaceTyCon, tidyToIfaceTcArgs)
+
 import GhcPrelude
 
+import IfaceType
 import TyCoRep
 import Type
 import TyCon
@@ -170,13 +173,14 @@ Defined here to avoid module loops. CoAxiom is loaded very early on.
 pprCoAxiom :: CoAxiom br -> SDoc
 pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
   = hang (text "axiom" <+> ppr ax <+> dcolon)
-       2 (vcat (map (ppr_co_ax_branch (\_ ty -> equals <+> pprType ty) ax) $
+       2 (vcat (map (ppr_co_ax_branch (\env _ ty ->
+                      equals <+> pprPrecTypeX env topPrec ty) ax) $
                     fromBranches branches))
 
 pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
 pprCoAxBranch = ppr_co_ax_branch pprRhs
   where
-    pprRhs fam_tc rhs
+    pprRhs _ fam_tc rhs
       | isDataFamilyTyCon fam_tc
       = empty -- Don't bother printing anything for the RHS of a data family
               -- instance...
@@ -190,7 +194,8 @@ pprCoAxBranch = ppr_co_ax_branch pprRhs
 pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
 pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
 
-ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
+ppr_co_ax_branch :: (TidyEnv -> TyCon -> Type -> SDoc)
+                 -> CoAxiom br -> CoAxBranch -> SDoc
 ppr_co_ax_branch ppr_rhs
               (CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
               (CoAxBranch { cab_tvs = tvs
@@ -199,8 +204,8 @@ ppr_co_ax_branch ppr_rhs
                           , cab_rhs = rhs
                           , cab_loc = loc })
   = foldr1 (flip hangNotEmpty 2)
-        [ pprUserForAll (mkTyCoVarBinders Inferred (ee_tvs ++ cvs))
-        , pprTypeApp fam_tc ee_lhs <+> ppr_rhs fam_tc rhs
+        [ pprUserForAll (mkTyCoVarBinders Inferred (ee_tvs' ++ cvs))
+        , pp_lhs <+> ppr_rhs env fam_tc ee_rhs
         , text "-- Defined" <+> pprLoc loc ]
   where
         pprLoc loc
@@ -211,10 +216,14 @@ ppr_co_ax_branch ppr_rhs
           = text "in" <+>
               quotes (ppr (nameModule name))
 
-        -- Eta-expand LHS types, because sometimes data family instances
-        -- are eta-reduced.
+        -- Eta-expand LHS and RHS 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
+        (ee_tvs, ee_lhs, ee_rhs) = etaExpandFamInst tvs lhs rhs
+
+        (env, ee_tvs') = tidyVarBndrs emptyTidyEnv ee_tvs
+        pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
+                                         (tidyToIfaceTcArgs env fam_tc ee_lhs)
 
 {-
 %************************************************************************
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 6180bf12b2..d727250c00 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -7,7 +7,7 @@
 module FamInstEnv (
         FamInst(..), FamFlavor(..), famInstAxiom, famInstTyCon, famInstRHS,
         famInstsRepTyCons, famInstRepTyCon_maybe, dataFamInstRepTyCon,
-        etaExpandFamInstLHS,
+        etaExpandFamInst,
         pprFamInst, pprFamInsts,
         mkImportedFamInst,
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index d6c0f33e04..5f70206a1a 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -61,7 +61,7 @@ module TyCoRep (
         pickLR,
 
         -- * Pretty-printing
-        pprType, pprParendType, pprPrecType,
+        pprType, pprParendType, pprPrecType, pprPrecTypeX,
         pprTypeApp, pprTCvBndr, pprTCvBndrs,
         pprSigmaType,
         pprTheta, pprParendTheta, pprForAll, pprUserForAll,
@@ -3122,11 +3122,14 @@ pprType       = pprPrecType topPrec
 pprParendType = pprPrecType appPrec
 
 pprPrecType :: PprPrec -> Type -> SDoc
-pprPrecType prec ty
+pprPrecType = pprPrecTypeX emptyTidyEnv
+
+pprPrecTypeX :: TidyEnv -> PprPrec -> Type -> SDoc
+pprPrecTypeX env prec ty
   = getPprStyle $ \sty ->
     if debugStyle sty           -- Use pprDebugType when in
     then debug_ppr_ty prec ty   -- when in debug-style
-    else pprPrecIfaceType prec (tidyToIfaceTypeSty ty sty)
+    else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
 
 pprTyLit :: TyLit -> SDoc
 pprTyLit = pprIfaceTyLit . toIfaceTyLit
@@ -3135,22 +3138,25 @@ pprKind, pprParendKind :: Kind -> SDoc
 pprKind       = pprType
 pprParendKind = pprParendType
 
-tidyToIfaceTypeSty :: Type -> PprStyle -> IfaceType
-tidyToIfaceTypeSty ty sty
-  | userStyle sty = tidyToIfaceType ty
+tidyToIfaceTypeStyX :: TidyEnv -> Type -> PprStyle -> IfaceType
+tidyToIfaceTypeStyX env ty sty
+  | userStyle sty = tidyToIfaceTypeX env ty
   | otherwise     = toIfaceTypeX (tyCoVarsOfType ty) ty
      -- in latter case, don't tidy, as we'll be printing uniques.
 
 tidyToIfaceType :: Type -> IfaceType
+tidyToIfaceType = tidyToIfaceTypeX emptyTidyEnv
+
+tidyToIfaceTypeX :: TidyEnv -> Type -> IfaceType
 -- It's vital to tidy before converting to an IfaceType
 -- or nested binders will become indistinguishable!
 --
 -- Also for the free type variables, tell toIfaceTypeX to
 -- leave them as IfaceFreeTyVar.  This is super-important
 -- for debug printing.
-tidyToIfaceType ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env ty)
+tidyToIfaceTypeX env ty = toIfaceTypeX (mkVarSet free_tcvs) (tidyType env' ty)
   where
-    env       = tidyFreeTyCoVars emptyTidyEnv free_tcvs
+    env'      = tidyFreeTyCoVars env free_tcvs
     free_tcvs = tyCoVarsOfTypeWellScoped ty
 
 ------------
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index ba41388081..6df6d944ed 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -69,7 +69,7 @@ module Type (
 
         modifyJoinResTy, setJoinResTy,
 
-        etaExpandFamInstLHS,
+        etaExpandFamInst,
 
         -- Analyzing types
         TyCoMapper(..), mapType, mapCoercion,
@@ -3054,29 +3054,26 @@ setJoinResTy ar 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)@.
+-- * Return the eta-expanded type variables, left-hand types, and right-hand
+--   type (if dealing with a data family instance). This function obtains the
+--   eta-reduced variables from the instance's representation 'TyCon' (which
+--   heads the right-hand type).
 --
--- * Just return the type variables and left-hand types (if dealing with a
---   type family instance).
+-- * Just return the type variables, left-hand types, and right-hand type
+--   (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).
+-- For an explanation of why data family instances need to be eta expanded, see
+-- @Note [Eta reduction for data families]@ in "FamInstEnv".
 
 -- 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
+etaExpandFamInst
   :: [TyVar] -- ^ The type variables
   -> [Type]  -- ^ The left-hand side types
   -> Type    -- ^ The right-hand side type
-  -> ([TyVar], [Type])
-etaExpandFamInstLHS tvs lhs rhs
+  -> ([TyVar], [Type], Type)
+etaExpandFamInst tvs lhs rhs
   | Just (tycon, tc_args) <- splitTyConApp_maybe rhs
   , isFamInstTyCon tycon
   = let tc_tvs           = tyConTyVars tycon
@@ -3084,9 +3081,10 @@ etaExpandFamInstLHS tvs lhs rhs
         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)
+        eta_expanded_rhs = mkAppTys rhs etad_tys
+    in (eta_expanded_tvs, eta_expanded_lhs, eta_expanded_rhs)
   | otherwise
-  = (tvs, lhs)
+  = (tvs, lhs, rhs)
 
 {-
 %************************************************************************
diff --git a/testsuite/tests/deSugar/should_run/T5472.stdout b/testsuite/tests/deSugar/should_run/T5472.stdout
deleted file mode 100644
index 0519ecba6e..0000000000
--- a/testsuite/tests/deSugar/should_run/T5472.stdout
+++ /dev/null
@@ -1 +0,0 @@
- 
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.hs b/testsuite/tests/indexed-types/should_compile/T15852.hs
new file mode 100644
index 0000000000..65c4ae68bc
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15852.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15852 where
+
+import Data.Kind
+import Data.Proxy
+
+data family DF a (b :: k)
+data instance DF (Proxy c) :: Proxy j -> Type
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
new file mode 100644
index 0000000000..bc5fd2a72e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15852.stderr
@@ -0,0 +1,13 @@
+TYPE CONSTRUCTORS
+  type role DF nominal nominal nominal
+  DF :: forall k. * -> k -> *
+COERCION AXIOMS
+  axiom T15852.D:R:DFProxyProxy0 ::
+    forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
+      DF (Proxy c) a = T15852.R:DFProxyProxy k1 k2 c j a
+        -- Defined at T15852.hs:10:15
+FAMILY INSTANCES
+  data instance DF (Proxy c) c j a
+Dependent modules: []
+Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
+                     integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5725c96507..551d382912 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -296,3 +296,4 @@ test('T15352', normal, compile, [''])
 test('T15664', normal, compile, [''])
 test('T15704', normal, compile, [''])
 test('T15711', normal, compile, ['-ddump-types'])
+test('T15852', normal, compile, ['-ddump-types'])
diff --git a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
index 58f423c163..12982a740c 100644
--- a/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
@@ -6,7 +6,7 @@ TYPE CONSTRUCTORS
   Sing :: forall k. k -> *
 COERCION AXIOMS
   axiom DataFamilyInstanceLHS.D:R:SingMyKind_0 ::
-    Sing _ = DataFamilyInstanceLHS.R:SingMyKind_
+    Sing _1 = DataFamilyInstanceLHS.R:SingMyKind_ _1
       -- Defined at DataFamilyInstanceLHS.hs:8:15
 DATA CONSTRUCTORS
   A :: MyKind
diff --git a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
index a075b34ea4..1cd0417e54 100644
--- a/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
@@ -4,7 +4,7 @@ TYPE CONSTRUCTORS
   Sing :: forall k. k -> *
 COERCION AXIOMS
   axiom NamedWildcardInDataFamilyInstanceLHS.D:R:SingMyKind_a0 ::
-    Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a
+    Sing _a = NamedWildcardInDataFamilyInstanceLHS.R:SingMyKind_a _a
       -- Defined at NamedWildcardInDataFamilyInstanceLHS.hs:8:15
 DATA CONSTRUCTORS
   A :: MyKind
diff --git a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
index 76c5b3fbc3..ae82437e1d 100644
--- a/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
@@ -4,13 +4,13 @@ TYPE CONSTRUCTORS
   type role F nominal nominal
   F :: * -> * -> *
 COERCION AXIOMS
-  axiom TypeFamilyInstanceLHS.D:R:FBool_ ::
-    F Bool _ = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15
-  axiom TypeFamilyInstanceLHS.D:R:FInt_ ::
-    F Int _ = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15
+  axiom TypeFamilyInstanceLHS.D:R:FBool_1 ::
+    F Bool _1 = Bool -- Defined at TypeFamilyInstanceLHS.hs:8:15
+  axiom TypeFamilyInstanceLHS.D:R:FInt_1 ::
+    F Int _1 = Int -- Defined at TypeFamilyInstanceLHS.hs:7:15
 FAMILY INSTANCES
-  type instance F Int _
-  type instance F Bool _
+  type instance F Int _1
+  type instance F Bool _1
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]