From b8d40af138fe0f7fad9b6afafe2152d8213a3e25 Mon Sep 17 00:00:00 2001
From: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
Date: Fri, 19 Feb 2021 19:43:30 +0100
Subject: [PATCH] Fix assertion error with linear types, #19400
The previous code using TyCoMapper could promote the same metavar twice.
Use a set instead.
---
compiler/GHC/Tc/Utils/Env.hs | 21 +++++++------------
.../tests/linear/should_compile/T19400.hs | 14 +++++++++++++
testsuite/tests/linear/should_compile/all.T | 1 +
3 files changed, 23 insertions(+), 13 deletions(-)
create mode 100644 testsuite/tests/linear/should_compile/T19400.hs
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 8dcb0b47f7d9..526bb489acd4 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -102,7 +102,6 @@ import GHC.Core.ConLike
import GHC.Core.TyCon
import GHC.Core.Type
import GHC.Core.Coercion.Axiom
-import GHC.Core.Coercion
import GHC.Core.Class
import GHC.Unit.Module
@@ -663,8 +662,7 @@ tcCheckUsage name id_mult thing_inside
; wrapper <- case actual_u of
Bottom -> return idHsWrapper
Zero -> tcSubMult (UsageEnvironmentOf name) Many id_mult
- MUsage m -> do { m <- zonkTcType m
- ; m <- promote_mult m
+ MUsage m -> do { m <- promote_mult m
; tcSubMult (UsageEnvironmentOf name) m id_mult }
; tcEmitBindingUsage (deleteUE uenv name)
; return wrapper }
@@ -690,16 +688,13 @@ tcCheckUsage name id_mult thing_inside
-- so we can't use it here. Thus, this dirtiness.
--
-- It works nicely in practice.
- (promote_mult, _, _, _) = mapTyCo mapper
- mapper = TyCoMapper { tcm_tyvar = \ () tv -> if isMetaTyVar tv
- then do { tclvl <- getTcLevel
- ; _ <- promoteMetaTyVarTo tclvl tv
- ; zonkTcTyVar tv }
- else return (mkTyVarTy tv)
- , tcm_covar = \ () cv -> return (mkCoVarCo cv)
- , tcm_hole = \ () h -> return (mkHoleCo h)
- , tcm_tycobinder = \ () tcv _flag -> return ((), tcv)
- , tcm_tycon = return }
+ --
+ -- We use a set to avoid calling promoteMetaTyVarTo twice on the same
+ -- metavariable. This happened in #19400.
+ promote_mult m = do { fvs <- zonkTyCoVarsAndFV (tyCoVarsOfType m)
+ ; any_promoted <- promoteTyVarSet fvs
+ ; if any_promoted then zonkTcType m else return m
+ }
{- *********************************************************************
* *
diff --git a/testsuite/tests/linear/should_compile/T19400.hs b/testsuite/tests/linear/should_compile/T19400.hs
new file mode 100644
index 000000000000..360c2358a225
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/T19400.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE ExistentialQuantification, LambdaCase, LinearTypes #-}
+
+module T19400 where
+
+data Stream = forall s. Stream (Either s s)
+
+f :: x %m -> y %m -> Int
+f x y = f x y
+
+step' :: () -> Stream -> Int
+step' x (Stream s) =
+ (\case
+ Left y -> f x y
+ Right y -> f x y) s
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index cea6db8d7341..fd44aef367e9 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -36,3 +36,4 @@ test('LinearTH2', normal, compile, [''])
test('LinearTH3', normal, compile, [''])
test('LinearHole', normal, compile, [''])
test('T18731', normal, compile, [''])
+test('T19400', unless(compiler_debugged(), skip), compile, [''])
--
GitLab