From 69c7b04394d48883cbad817734917a5f0c77de15 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 3 Jul 2019 08:55:26 +0100 Subject: 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 078ebecd54..35f4d00f39 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 0000000000..70fc7bd742 --- /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 0000000000..e265866119 --- /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 5a90ebe723..c67d80d621 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, ['']) -- cgit v1.2.1