diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-11-14 09:16:22 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-11-14 11:12:33 +0000 |
commit | 0a85190312a1de3d300912051309b94589c08683 (patch) | |
tree | 12dfdeb728e0782adad5c05980d858669ad01e3e | |
parent | e3ec2e7ae94524ebd111963faf34b84d942265b4 (diff) | |
download | haskell-0a85190312a1de3d300912051309b94589c08683.tar.gz |
Fix a TyVar bug in the flattener
A year ago I gave up on trying to rigorously separate TyVars
from TcTyVars, and instead allowed TyVars to appear rather more
freely in types examined by the constraint solver:
commit 18d0bdd3848201882bae167e3b15fd797d217e93
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed Nov 23 16:00:00 2016 +0000
Allow TyVars in TcTypes
See Note [TcTyVars in the typechecker] in TcType.
However, TcFlatten.flatten_tyvar1 turned out to treat
a TyVar specially, and implicitly assumed that it could
not have an equality constraint in the inert set. Wrong!
This caused Trac #14450. Fortunately it is easily fixed,
by deleting code.
-rw-r--r-- | compiler/typecheck/TcFlatten.hs | 7 | ||||
-rw-r--r-- | compiler/typecheck/TcType.hs | 4 | ||||
-rw-r--r-- | compiler/typecheck/TcUnify.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T14450.hs | 31 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T14450.stderr | 8 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 1 |
6 files changed, 46 insertions, 7 deletions
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 3c44cde47f..c8479a6d06 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -1371,15 +1371,10 @@ flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult -- See also the documentation for FlattenTvResult flatten_tyvar1 tv - | not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty) - = return FTRNotFollowed - -- So ty contains references to the non-TcTyVar a - - | otherwise = do { mb_ty <- liftTcS $ isFilledMetaTyVar_maybe tv - ; role <- getRole ; case mb_ty of Just ty -> do { traceFlat "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) + ; role <- getRole ; return (FTRFollowed ty (mkReflCo role ty)) } ; Nothing -> do { traceFlat "Unfilled tyvar" (ppr tv) ; fr <- getFlavourRole diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 5e1e4be99f..d781aec49c 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -294,6 +294,10 @@ reasons: solve any kind equalities in foo's signature. So the solver may see free occurrences of 'k'. + See calls to tcExtendTyVarEnv for other places that ordinary + TyVars are bought into scope, and hence may show up in the types + and inds generated by TcHsType. + It's convenient to simply treat these TyVars as skolem constants, which of course they are. So diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 926db6e65b..0b2151b8e1 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -1814,7 +1814,7 @@ matchExpectedFunKind hs_ty = go go k | Just k' <- tcView k = go k' go k@(TyVarTy kvar) - | isTcTyVar kvar, isMetaTyVar kvar + | isMetaTyVar kvar = do { maybe_kind <- readMetaTyVar kvar ; case maybe_kind of Indirect fun_kind -> go fun_kind diff --git a/testsuite/tests/polykinds/T14450.hs b/testsuite/tests/polykinds/T14450.hs new file mode 100644 index 0000000000..3b8f5b7e70 --- /dev/null +++ b/testsuite/tests/polykinds/T14450.hs @@ -0,0 +1,31 @@ +{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-} + +module T14450 where + +import Data.Kind + +data TyFun :: Type -> Type -> Type + +type a ~> b = TyFun a b -> Type + +type Cat ob = ob -> ob -> Type + +type SameKind (a :: k) (b :: k) = (() :: Constraint) + +type family Apply (f :: a ~> b) (x :: a) :: b where + Apply IddSym0 x = Idd x + +class Varpi (f :: i ~> j) where + type Dom (f :: i ~> j) :: Cat i + type Cod (f :: i ~> j) :: Cat j + + varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a') + +type family Idd (a::k) :: k where + Idd (a::k) = a + +data IddSym0 :: k ~> k where + IddSym0KindInference :: IddSym0 l + +instance Varpi (IddSym0 :: k ~> k) where + type Dom (IddSym0 :: Type ~> Type) = (->) diff --git a/testsuite/tests/polykinds/T14450.stderr b/testsuite/tests/polykinds/T14450.stderr new file mode 100644 index 0000000000..c7caf04220 --- /dev/null +++ b/testsuite/tests/polykinds/T14450.stderr @@ -0,0 +1,8 @@ + +T14450.hs:31:12: error: + • Expected kind ‘k ~> k’, + but ‘(IddSym0 :: Type ~> Type)’ has kind ‘* ~> *’ + • In the first argument of ‘Dom’, namely + ‘(IddSym0 :: Type ~> Type)’ + In the type instance declaration for ‘Dom’ + In the instance declaration for ‘Varpi (IddSym0 :: k ~> k)’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 66bd9b13df..73408e81d9 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -173,3 +173,4 @@ test('T14265', normal, compile_fail, ['']) test('T13391', normal, compile_fail, ['']) test('T13391a', normal, compile, ['']) test('T14270', normal, compile, ['']) +test('T14450', normal, compile_fail, ['']) |