diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2019-07-03 08:55:26 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2019-07-04 21:23:49 -0400 |
commit | 53aa59f36dc6554c37ead9677c71e91cad3f9f21 (patch) | |
tree | ce78eedab239b1ec96e0e78d7ebba5b1f3fee5e5 | |
parent | 679427f878e50ba5a9981bac4c2f9c76f4de3c3c (diff) | |
download | haskell-53aa59f36dc6554c37ead9677c71e91cad3f9f21.tar.gz |
Add a missing zonk (fixes #16902)
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’
-rw-r--r-- | compiler/typecheck/TcUnify.hs | 32 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T16902.hs | 11 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T16902.stderr | 6 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 1 |
4 files changed, 40 insertions, 10 deletions
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, ['']) |