Improve inference with linear typeswip/linear-backports-9.0

This fixes test Linear14. The code in Unify.hs was always using
multiplicity Many instead of a new metavariable.

(cherry picked from commit 65721691ce9c4107d1cf84ad131bf167a9e42a7d)

4 files changed, 15 insertions, 12 deletions

diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index bf933127b8..f11c160ebe 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -212,12 +212,12 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
     ------------
     defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
     defer acc_arg_tys n fun_ty
-      = do { more_arg_tys <- replicateM n newInferExpType
+      = do { more_arg_tys <- replicateM n (mkScaled <$> newFlexiTyVarTy multiplicityTy <*> newInferExpType)
            ; res_ty       <- newInferExpType
-           ; result       <- thing_inside (reverse acc_arg_tys ++ (map unrestricted more_arg_tys)) res_ty
-           ; more_arg_tys <- mapM readExpType more_arg_tys
+           ; result       <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty
+           ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
            ; res_ty       <- readExpType res_ty
-           ; let unif_fun_ty = mkVisFunTysMany more_arg_tys res_ty
+           ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
            ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
                          -- Not a good origin at all :-(
            ; return (wrap, result) }
@@ -339,9 +339,10 @@ matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty
     defer fun_ty
       = do { arg_ty <- newOpenFlexiTyVarTy
            ; res_ty <- newOpenFlexiTyVarTy
-           ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty
+           ; mult <- newFlexiTyVarTy multiplicityTy
+           ; let unif_fun_ty = mkVisFunTy mult arg_ty res_ty
            ; co <- unifyType mb_thing fun_ty unif_fun_ty
-           ; return (mkWpCastN co, unrestricted arg_ty, res_ty) }
+           ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
 
     ------------
     mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
index 219f2879b0..b05335047f 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 136961
+  Total ticks: 140801
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index 7f0e045db1..764d8a1f45 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -16,7 +16,7 @@ test('TupSection', normal, compile, [''])
 test('Pr110', normal, compile, [''])
 test('Linear10', normal, compile, [''])
 test('Linear12', normal, compile, [''])
-test('Linear14', expect_broken(298), compile, [''])
+test('Linear14', normal, compile, [''])
 test('Linear15', normal, compile, [''])
 test('Linear16', normal, compile, [''])
 test('Linear3', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr
index 15e9cc4658..c599b276d9 100644
--- a/testsuite/tests/typecheck/should_fail/T7869.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7869.stderr
@@ -1,16 +1,18 @@
 
 T7869.hs:3:12: error:
-    • Couldn't match type ‘b1’ with ‘b’
+    • Couldn't match type ‘a1’ with ‘a’
       Expected: [a1] -> b1
         Actual: [a] -> b
-      ‘b1’ is a rigid type variable bound by
+      ‘a1’ is a rigid type variable bound by
         an expression type signature:
           forall a1 b1. [a1] -> b1
         at T7869.hs:3:20-27
-      ‘b’ is a rigid type variable bound by
+      ‘a’ is a rigid type variable bound by
         the inferred type of f :: [a] -> b
         at T7869.hs:3:1-27
     • In the expression: f x
       In the expression: (\ x -> f x) :: [a] -> b
       In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
-    • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
+    • Relevant bindings include
+        x :: [a1] (bound at T7869.hs:3:7)
+        f :: [a] -> b (bound at T7869.hs:3:1)