Apply the right substitution in ty-fam improvement

Trac #13135 showed that we were failing to apply the
correct substitution to the un-substituted tyvars during
type-family improvement using injectivity.  Specifically
in TcInteractlinjImproveEqns we need to use instFlexiX.

An outright bug, easy to fix.

Slight refactoring along the way.  The quantified tyars of the axiom are
readily to hand; we don't need to take the free tyvars of the LHS

3 files changed, 133 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_fail/T13135.hs b/testsuite/tests/dependent/should_fail/T13135.hs
new file mode 100644
index 0000000000..c39b3f5842
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13135.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+
+
+module T12135 where
+
+
+import Data.Kind (Type)
+
+
+class sub :<: sup
+  where
+    -- | Injection from @sub@ to @sup@
+    inj ::  sub sig -> sup sig
+
+instance (sub :<: sup) => (sub :<: AST sup)
+  where
+    inj = Sym . inj
+
+
+data Sig a = Full a | (:->) a (Sig a)
+
+infixr :->
+
+type Sym t = (Sig t -> Type)
+
+data AST :: Sym t -> Sym t
+  where
+    Sym  :: sym sig -> AST sym sig
+    (:$) :: AST sym (a :-> sig) -> AST sym (Full a) -> AST sym sig
+
+-- | Generic N-ary syntactic construct
+--
+-- 'Construct' gives a quick way to introduce a syntactic construct by giving its name and semantic
+-- function.
+data Constr sig = Constr String
+
+smartSym :: (sub :<: sup) => sub sig -> SmartFun sup sig
+smartSym = error "urk"
+
+type family   SmartFun (sym :: Sig t -> Type) sig = f | f -> sym sig  where
+-- In full glory:
+-- type family SmartFun {t} (sym :: Sig t -> Type) (sig :: Sig t) :: *
+--            = f | f -> {t} sym sig  where
+  SmartFun sym (Full a)    = AST sym (Full a)
+  SmartFun sym (a :-> sig) = AST sym (Full a) -> SmartFun sym sig
+
+-- | Get the length of an array
+arrLen ::  AST Constr (Full [a]) -> AST Constr (Full Int)
+arrLen = smartSym sym where
+  sym = Constr "arrLen"
+
+
+
+{- The original bug was a familure to subsitute
+   properly during type-function improvement.
+
+--------------------------------------
+doTopReact
+  [WD] hole{a1y1} {0}:: (SmartFun
+                           t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2] :: *)
+                        GHC.Prim.~#
+                        (s_a1y0[fuv:0] :: *) (CFunEqCan)
+matchFamTcM
+  Matching: SmartFun t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2]
+  Match failed
+improveTopFunEqs
+  SmartFun [t_a1x9[tau:2], sup_a1xb[tau:2],
+            sig_a1xc[tau:2]] s_a1y0[fuv:0]
+  [* ~ t_a1x9[tau:2], Constr (Sig *) ~ sup_a1xb[tau:2],
+   (':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] ~ sig_a1xc[tau:2]]
+
+Emitting new derived equality
+  [D] _ {0}:: (* :: *) GHC.Prim.~# (t_a1x9[tau:2] :: *)
+  [D] _ {0}:: (Constr (Sig *) :: (Sig * -> *))
+                GHC.Prim.~#
+              (sup_a1xb[tau:2] :: (Sig t_a1x9[tau:2] -> *))
+  [D] _ {0}:: ((':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] :: Sig *)
+              GHC.Prim.~#
+              (sig_a1xc[tau:2] :: Sig t_a1x9[tau:2])
+
+but sig_a1y3 :: Sig t   BAD
+--------------------------------------
+
+Instance
+  forall t (sig :: Sig t) (a :: t) (sym :: Sig t -> *).
+    SmartFun t sym ((:->) t a sig) = AST t sym (Full t a) -> SmartFun t sym sig
+
+Wanted:
+  SmartFun t_a1x9[tau:2] sup_a1xb[tau:2] sig_a1xc[tau:2] ~ s_a1y0[fuv:0]
+  s_a1y0[fuv:0]  ~  AST * (Constr (Sig *))
+                          ('Full * [a_a1wT[sk:2]])
+                    -> AST * (Constr (Sig *)) ('Full * Int)
+
+Substitution after matching RHSs
+  [ t -> *
+  , (sym :: Sig t -> *) -> Constr (Sig *)
+  , a -> a_a1wT ]
+
+add sig -> sig0 :: Sig t   -- Or rather Sig *
+
+Apply to LHS
+
+   SmartFun * (Constr (Sig *)) ((:->) * a_a1wT sig0)
+
+
+improveTopFunEqs
+  SmartFun [t_a1x9[tau:2], sup_a1xb[tau:2],
+            sig_a1xc[tau:2]] s_a1y0[fuv:0]
+  [* ~ t_a1x9[tau:2], Constr (Sig *) ~ sup_a1xb[tau:2],
+   (':->) * [a_a1wT[sk:2]] sig_a1y3[tau:2] ~ sig_a1xc[tau:2]]
+-}
diff --git a/testsuite/tests/dependent/should_fail/T13135.stderr b/testsuite/tests/dependent/should_fail/T13135.stderr
new file mode 100644
index 0000000000..88de56943e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13135.stderr
@@ -0,0 +1,10 @@
+
+T13135.hs:60:10: error:
+    • No instance for (Constr :<: Constr)
+        arising from a use of ‘smartSym’
+    • In the expression: smartSym sym
+      In an equation for ‘arrLen’:
+          arrLen
+            = smartSym sym
+            where
+                sym = Constr "arrLen"
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index b9c82f131b..c648f9ed1d 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -16,3 +16,4 @@ test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
 test('T12174', normal, compile_fail, [''])
 test('T12081', normal, compile_fail, [''])
+test('T13135', normal, compile_fail, [''])