From 53aa59f36dc6554c37ead9677c71e91cad3f9f21 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed, 3 Jul 2019 08:55:26 +0100
Subject: [PATCH] Add a missing zonk (fixes #16902)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
In the eager unifier, when unifying (tv1 ~ tv2),
when we decide to swap them over, to unify (tv2 ~ tv1),
I'd forgotten to ensure that tv1's kind was fully zonked,
which is an invariant of uUnfilledTyVar2.
That could lead us to build an infinite kind, or (in the
case of #16902) update the same unification variable twice.
Yikes.
Now we get an error message rather than non-termination,
which is much better. The error message is not great,
but it's a very strange program, and I can't see an easy way
to improve it, so for now I'm just committing this fix.
Here's the decl
data F (a :: k) :: (a ~~ k) => Type where
MkF :: F a
and the rather error message of which I am not proud
T16902.hs:11:10: error:
• Expected a type, but found something with kind ‘a1’
• In the type ‘F a’
---
compiler/typecheck/TcUnify.hs | 32 +++++++++++++++++--------
testsuite/tests/polykinds/T16902.hs | 11 +++++++++
testsuite/tests/polykinds/T16902.stderr | 6 +++++
testsuite/tests/polykinds/all.T | 1 +
4 files changed, 40 insertions(+), 10 deletions(-)
create mode 100644 testsuite/tests/polykinds/T16902.hs
create mode 100644 testsuite/tests/polykinds/T16902.stderr
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 078ebecd5402..35f4d00f3981 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1388,7 +1388,7 @@ uType t_or_k origin orig_ty1 orig_ty2
= do { co_tys <- uType t_or_k origin t1 t2
; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
- -- Variables; go for uVar
+ -- Variables; go for uUnfilledVar
-- Note that we pass in *original* (before synonym expansion),
-- so that type variables tend to get filled in with
-- the most informative version of the type
@@ -1576,11 +1576,11 @@ improve error messages.
************************************************************************
* *
- uVar and friends
+ uUnfilledVar and friends
* *
************************************************************************
-@uVar@ is called when at least one of the types being unified is a
+@uunfilledVar@ is called when at least one of the types being unified is a
variable. It does {\em not} assume that the variable is a fixed point
of the substitution; rather, notice that @uVar@ (defined below) nips
back into @uTys@ if it turns out that the variable is already bound.
@@ -1590,7 +1590,8 @@ back into @uTys@ if it turns out that the variable is already bound.
uUnfilledVar :: CtOrigin
-> TypeOrKind
-> SwapFlag
- -> TcTyVar -- Tyvar 1
+ -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
+ -- definitely not a /filled/ meta-tyvar
-> TcTauType -- Type 2
-> TcM Coercion
-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
@@ -1608,7 +1609,8 @@ uUnfilledVar origin t_or_k swapped tv1 ty2
uUnfilledVar1 :: CtOrigin
-> TypeOrKind
-> SwapFlag
- -> TcTyVar -- Tyvar 1
+ -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
+ -- definitely not a /filled/ meta-tyvar
-> TcTauType -- Type 2, zonked
-> TcM Coercion
uUnfilledVar1 origin t_or_k swapped tv1 ty2
@@ -1621,12 +1623,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
where
-- 'go' handles the case where both are
-- tyvars so we might want to swap
+ -- E.g. maybe tv2 is a meta-tyvar and tv1 is not
go tv2 | tv1 == tv2 -- Same type variable => no-op
= return (mkNomReflCo (mkTyVarTy tv1))
| swapOverTyVars tv1 tv2 -- Distinct type variables
- = uUnfilledVar2 origin t_or_k (flipSwap swapped)
- tv2 (mkTyVarTy tv1)
+ -- Swap meta tyvar to the left if poss
+ = do { tv1 <- zonkTyCoVarKind tv1
+ -- We must zonk tv1's kind because that might
+ -- not have happened yet, and it's an invariant of
+ -- uUnfilledTyVar2 that ty2 is fully zonked
+ -- Omitting this caused #16902
+ ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
+ tv2 (mkTyVarTy tv1) }
| otherwise
= uUnfilledVar2 origin t_or_k swapped tv1 ty2
@@ -1635,7 +1644,8 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
uUnfilledVar2 :: CtOrigin
-> TypeOrKind
-> SwapFlag
- -> TcTyVar -- Tyvar 1
+ -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar
+ -- definitely not a /filled/ meta-tyvar
-> TcTauType -- Type 2, zonked
-> TcM Coercion
uUnfilledVar2 origin t_or_k swapped tv1 ty2
@@ -1652,8 +1662,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
, ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2)
, ppr (isTcReflCo co_k), ppr co_k ]
- ; if isTcReflCo co_k -- only proceed if the kinds matched.
-
+ ; if isTcReflCo co_k
+ -- Only proceed if the kinds match
+ -- NB: tv1 should still be unfilled, despite the kind unification
+ -- because tv1 is not free in ty2 (or, hence, in its kind)
then do { writeMetaTyVar tv1 ty2'
; return (mkTcNomReflCo ty2') }
diff --git a/testsuite/tests/polykinds/T16902.hs b/testsuite/tests/polykinds/T16902.hs
new file mode 100644
index 000000000000..70fc7bd742af
--- /dev/null
+++ b/testsuite/tests/polykinds/T16902.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind
+import Data.Type.Equality
+
+data F (a :: k) :: (a ~~ k) => Type where
+ MkF :: F a
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
new file mode 100644
index 000000000000..e26586611990
--- /dev/null
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -0,0 +1,6 @@
+
+T16902.hs:11:10: error:
+ • Expected a type, but found something with kind ‘a1’
+ • In the type ‘F a’
+ In the definition of data constructor ‘MkF’
+ In the data declaration for ‘F’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 5a90ebe72315..c67d80d621a0 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -211,3 +211,4 @@ test('T16221', normal, compile, [''])
test('T16221a', normal, compile_fail, [''])
test('T16342', normal, compile, [''])
test('T16263', normal, compile_fail, [''])
+test('T16902', normal, compile_fail, [''])
--
GitLab