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

7 files changed, 32 insertions, 9 deletions

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]