anyRewritableTyVar now looks in RuntimeReps

Previously, anyRewritableTyVar looked only at the arg and res
of `arg -> res`, but their RuntimeReps are also subject to
rewriting. Easy to fix.

Test case: typecheck/should_compile/T17024

Fixes #17024.

4 files changed, 36 insertions, 1 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index ba4efcf35d..65e77ab9da 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -853,6 +853,10 @@ anyRewritableTyVar :: Bool    -- Ignore casts and coercions
 anyRewritableTyVar ignore_cos role pred ty
   = go role emptyVarSet ty
   where
+    -- NB: No need to expand synonyms, because we can find
+    -- all free variables of a synonym by looking at its
+    -- arguments
+
     go_tv rl bvs tv | tv `elemVarSet` bvs = False
                     | otherwise           = pred rl tv
 
@@ -860,7 +864,10 @@ anyRewritableTyVar ignore_cos role pred ty
     go _ _     (LitTy {})        = False
     go rl bvs (TyConApp tc tys)  = go_tc rl bvs tc tys
     go rl bvs (AppTy fun arg)    = go rl bvs fun || go NomEq bvs arg
-    go rl bvs (FunTy _ arg res)  = go rl bvs arg || go rl bvs res
+    go rl bvs (FunTy _ arg res)  = go NomEq bvs arg_rep || go NomEq bvs res_rep ||
+                                   go rl bvs arg || go rl bvs res
+      where arg_rep = getRuntimeRep arg -- forgetting these causes #17024
+            res_rep = getRuntimeRep res
     go rl bvs (ForAllTy tv ty)   = go rl (bvs `extendVarSet` binderVar tv) ty
     go rl bvs (CastTy ty co)     = go rl bvs ty || go_co rl bvs co
     go rl bvs (CoercionTy co)    = go_co rl bvs co  -- ToDo: check
diff --git a/testsuite/tests/typecheck/should_compile/T17024.hs b/testsuite/tests/typecheck/should_compile/T17024.hs
new file mode 100644
index 0000000000..6ebc2f7a07
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17024.hs
@@ -0,0 +1,19 @@
+{-# language TypeFamilies, FunctionalDependencies, GADTs, DataKinds, TypeOperators, ScopedTypeVariables, FlexibleInstances , UndecidableInstances, PartialTypeSignatures #-}
+
+module T17024 where
+
+infixr 6 :::
+
+data HList xs where
+  HNil :: HList '[]
+  (:::) :: a -> HList as -> HList (a ': as)
+
+class AppHList ts o f | ts f -> o, ts o -> f where
+   appHList :: f -> HList ts -> o
+instance AppHList '[] o o where
+   appHList x HNil = x
+instance AppHList ts o f => AppHList (t : ts) o (t -> f) where
+   appHList f (x ::: xs) = appHList (f x) xs
+
+foo :: (a -> b -> c) -> HList '[a, b] -> _
+foo = appHList
diff --git a/testsuite/tests/typecheck/should_compile/T17024.stderr b/testsuite/tests/typecheck/should_compile/T17024.stderr
new file mode 100644
index 0000000000..c3d18ffd87
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17024.stderr
@@ -0,0 +1,8 @@
+
+T17024.hs:18:42: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘c’
+      Where: ‘c’ is a rigid type variable bound by
+               the inferred type of foo :: (a -> b -> c) -> HList '[a, b] -> c
+               at T17024.hs:18:1-42
+    • In the type ‘(a -> b -> c) -> HList '[a, b] -> _’
+      In the type signature: foo :: (a -> b -> c) -> HList '[a, b] -> _
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c1cd076a6d..467f7ea192 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -698,3 +698,4 @@ test('T12760', unless(compiler_debugged(), skip), compile, ['-O'])
 test('T13142', normal, compile, ['-O2'])
 test('T12926', reqlib('vector'), compile, ['-O2'])
 test('T17792', normal, compile, [''])
+test('T17024', normal, compile, [''])