diff options
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 53 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.hs | 40 | ||||
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 5 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/T7786.hs (renamed from testsuite/tests/indexed-types/should_fail/T7786.hs) | 0 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 2 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T7786.stderr | 48 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 2 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/tc141.stderr | 16 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T5689.stderr | 14 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T5691.stderr | 9 |
11 files changed, 68 insertions, 122 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 4188303860..007b970791 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1572,7 +1572,7 @@ kcLHsQTyVars name flav cusk | otherwise = do { (scoped_kvs, (tc_tvs, res_kind)) -- Why kcImplicitTKBndrs which uses newSigTyVar? - -- See Note [Kind generalisation and sigTvs] + -- See Note [Kind generalisation and SigTvs] <- kcImplicitTKBndrs kv_ns $ kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside @@ -2421,9 +2421,8 @@ tcHsPatSigType ctxt sig_ty new_tv = case ctxt of RuleSigCtxt {} -> newSkolemTyVar - _ -> newSigTyVar + _ -> newTauTyVar -- See Note [Pattern signature binders] - -- See Note [Unifying SigTvs] mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv ; return (tyVarName tv, tv') } @@ -2500,24 +2499,31 @@ patBindSigErr sig_tvs {- Note [Pattern signature binders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider - data T = forall a. T a (a->Int) - f (T x (f :: b->Int)) = blah + + data T where + MkT :: forall a. a -> (a -> Int) -> T + + f :: T -> ... + f (MkT x (f :: b -> c)) = ... Here - * The pattern (T p1 p2) creates a *skolem* type variable 'a_sk', + * The pattern (MkT p1 p2) creates a *skolem* type variable 'a_sk', It must be a skolem so that that it retains its identity, and TcErrors.getSkolemInfo can thereby find the binding site for the skolem. - * The type signature pattern (f :: b->Int) makes a fresh meta-tyvar b_sig - (a SigTv), and binds "b" :-> b_sig in the envt + * The type signature pattern (f :: b -> c) makes freshs meta-tyvars + beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the + environment - * Then unification makes b_sig := a_sk - That's why we must make b_sig a MetaTv (albeit a SigTv), - not a SkolemTv, so that it can unify to a_sk. + * Then unification makes beta := a_sk, gamma := Int + That's why we must make beta and gamma a MetaTv, + not a SkolemTv, so that it can unify to a_sk rsp. Int. + Note that gamma unifies with a type, not just a type variable + (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0029-scoped-type-variables-types.rst) - * Finally, in 'blah' we must have the envt "b" :-> a_sk. The pair - ("b" :-> a_sk) is returned by tcHsPatSigType, constructed by - mk_tv_pair in that function. + * Finally, in 'blah' we must have the envt "b" :-> a_sk, "c" :-> Int. + The pairs ("b" :-> a_sk, "c" :-> Int) are returned by tcHsPatSigType, + constructed by mk_tv_pair in that function. Another example (Trac #13881): fl :: forall (l :: [a]). Sing l -> Sing l @@ -2526,7 +2532,7 @@ When we reach the pattern signature, 'l' is in scope from the outer 'forall': "a" :-> a_sk :: * "l" :-> l_sk :: [a_sk] -We make up a fresh meta-SigTv, y_sig, for 'y', and kind-check +We make up a fresh meta-TauTv, y_sig, for 'y', and kind-check the pattern signature Sing (l :: [y]) That unifies y_sig := a_sk. We return from tcHsPatSigType with @@ -2538,23 +2544,6 @@ Here this really is the binding site of the type variable so we'd like to use a skolem, so that we get a complaint if we unify two of them together. -Note [Unifying SigTvs] -~~~~~~~~~~~~~~~~~~~~~~ -ALAS we have no decent way of avoiding two SigTvs getting unified. -Consider - f (x::(a,b)) (y::c)) = [fst x, y] -Here we'd really like to complain that 'a' and 'c' are unified. But -for the reasons above we can't make a,b,c into skolems, so they -are just SigTvs that can unify. And indeed, this would be ok, - f x (y::c) = case x of - (x1 :: a1, True) -> [x,y] - (x1 :: a2, False) -> [x,y,y] -Here the type of x's first component is called 'a1' in one branch and -'a2' in the other. We could try insisting on the same OccName, but -they definitely won't have the sane lexical Name. - -I think we could solve this by recording in a SigTv a list of all the -in-scope variables that it should not unify with, but it's fiddly. ************************************************************************ diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 80929d12d4..a44b5e0d2f 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -51,7 +51,7 @@ module TcMType ( -- Instantiation newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, newMetaSigTyVars, newMetaSigTyVarX, - newSigTyVar, newSkolemTyVar, newWildCardX, + newSigTyVar, newTauTyVar, newSkolemTyVar, newWildCardX, tcInstType, tcInstSkolTyVars,tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX, @@ -620,13 +620,28 @@ instead of the buggous ************************************************************************ -} --- a SigTv can unify with type *variables* only, including other SigTvs --- and skolems. Sometimes, they can unify with type variables that the --- user would rather keep distinct; see #11203 for an example. --- So, any client of this --- function needs to either allow the SigTvs to unify with each other --- (say, for pattern-bound scoped type variables), or check that they --- don't (say, with a call to findDubSigTvs). +{- +Note [SigTv] +~~~~~~~~~~~~ + +A SigTv can unify with type *variables* only, including other SigTvs and +skolems. Sometimes, they can unify with type variables that the user would +rather keep distinct; see #11203 for an example. So, any client of this +function needs to either allow the SigTvs to unify with each other or check +that they don't (say, with a call to findDubSigTvs). + +Before #15050 this was used for ScopedTypeVariables in patterns, to make sure +these type variables only refer to other type variables, but this restriction +was dropped, and ScopedTypeVariables can now refer to full types (GHC Proposal +29). + +The remaining uses of newSigTyVars are +* in kind signatures, see Note [Kind generalisation and SigTvs] + and Note [Use SigTvs in kind-checking pass] +* in partial type signatures, see Note [Quantified variables in partial type signatures] +-} + +-- see Note [SigTv] newSigTyVar :: Name -> Kind -> TcM TcTyVar newSigTyVar name kind = do { details <- newMetaDetails SigTv @@ -634,6 +649,7 @@ newSigTyVar name kind ; traceTc "newSigTyVar" (ppr tyvar) ; return tyvar } + -- makes a new skolem tv newSkolemTyVar :: Name -> Kind -> TcM TcTyVar newSkolemTyVar name kind = do { lvl <- getTcLevel @@ -807,6 +823,14 @@ coercion variables, except for the special case of the promoted Eq#. But, that can't ever appear in user code, so we're safe! -} +newTauTyVar :: Name -> Kind -> TcM TcTyVar +newTauTyVar name kind + = do { details <- newMetaDetails TauTv + ; let tyvar = mkTcTyVar name kind details + ; traceTc "newTauTyVar" (ppr tyvar) + ; return tyvar } + + mkMetaTyVarName :: Unique -> FastString -> Name -- Makes a /System/ Name, which is eagerly eliminated by -- the unifier; see TcUnify.nicer_to_update_tv1, and diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index d5cdf71ed0..30b3cf19c8 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -10430,11 +10430,6 @@ scope, because it is bound by the pattern match. The effect is to bring it into scope, standing for the existentially-bound type variable. -When a pattern type signature binds a type variable in this way, GHC -insists that the type variable is bound to a *rigid*, or fully-known, -type variable. This means that any user-written type signature always -stands for a completely known type. - It does seem odd that the existentially-bound type variable *must not* be already in scope. Contrast that usually name-bindings merely shadow (make a 'hole') in a same-named outer variable's scope. diff --git a/testsuite/tests/indexed-types/should_fail/T7786.hs b/testsuite/tests/indexed-types/should_compile/T7786.hs index 33a74f233f..33a74f233f 100644 --- a/testsuite/tests/indexed-types/should_fail/T7786.hs +++ b/testsuite/tests/indexed-types/should_compile/T7786.hs diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index 035c85d179..11b7bcbc16 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -280,6 +280,7 @@ test('T14237', normal, compile, ['']) test('T14554', normal, compile, ['']) test('T14680', normal, compile, ['']) test('T15057', normal, compile, ['']) +test('T7786', normal, compile, ['']) test('T15144', normal, compile, ['']) test('T15122', normal, compile, ['']) test('T13777', normal, compile, ['']) @@ -289,4 +290,3 @@ test('T15322', normal, compile, ['']) test('T15322a', normal, compile_fail, ['']) test('T15142', normal, compile, ['']) test('T15352', normal, compile, ['']) - diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr deleted file mode 100644 index a82a1ca2f7..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T7786.stderr +++ /dev/null @@ -1,48 +0,0 @@ - -T7786.hs:96:41: error: - • Couldn't match type ‘xxx’ - with ‘Intersect (BuriedUnder sub k 'Empty) inv’ - Expected type: Maybe (Sing xxx) - Actual type: Maybe - (Sing (Intersect (BuriedUnder sub k 'Empty) inv)) - • In a stmt of a 'do' block: Nil :: Sing xxx <- foogle db k sub - In the expression: - do Nil :: Sing xxx <- foogle db k sub - return $ Sub db k sub - In an equation for ‘addSub’: - addSub db k sub - = do Nil :: Sing xxx <- foogle db k sub - return $ Sub db k sub - • Relevant bindings include - sub :: Database sub (bound at T7786.hs:96:13) - k :: Sing k (bound at T7786.hs:96:11) - db :: Database inv (bound at T7786.hs:96:8) - addSub :: Database inv - -> Sing k - -> Database sub - -> Maybe (Database (BuriedUnder sub k inv)) - (bound at T7786.hs:96:1) - -T7786.hs:97:31: error: - • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv - ~ 'Empty - arising from a use of ‘Sub’ - from the context: xxx ~ 'Empty - bound by a pattern with constructor: Nil :: forall a. Sing 'Empty, - in a pattern binding in - a 'do' block - at T7786.hs:96:22-24 - • In the second argument of ‘($)’, namely ‘Sub db k sub’ - In a stmt of a 'do' block: return $ Sub db k sub - In the expression: - do Nil :: Sing xxx <- foogle db k sub - return $ Sub db k sub - • Relevant bindings include - sub :: Database sub (bound at T7786.hs:96:13) - k :: Sing k (bound at T7786.hs:96:11) - db :: Database inv (bound at T7786.hs:96:8) - addSub :: Database inv - -> Sing k - -> Database sub - -> Maybe (Database (BuriedUnder sub k inv)) - (bound at T7786.hs:96:1) diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index b8775554c9..11e9d0a65d 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -87,7 +87,6 @@ test('T7536', normal, compile_fail, ['']) test('T7729', normal, compile_fail, ['']) test('T7729a', normal, compile_fail, ['']) -test('T7786', normal, compile_fail, ['']) test('NoGood', normal, compile_fail, ['']) test('T7967', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 1857ba814e..aba8c9b46d 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -620,7 +620,7 @@ test('SplitWD', normal, compile, ['']) # (2) Build the program twice: once with -dynamic, and then # with -prof using -osuf to set a different object file suffix. test('T14441', omit_ways(['profasm']), compile, ['']) -test('T15050', [expect_broken(15050)], compile, ['']) +test('T15050', normal, compile, ['']) test('T14735', normal, compile, ['']) test('T15180', normal, compile, ['']) test('T15232', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr index b2fe9abb4b..f0cfdefd03 100644 --- a/testsuite/tests/typecheck/should_compile/tc141.stderr +++ b/testsuite/tests/typecheck/should_compile/tc141.stderr @@ -37,13 +37,13 @@ tc141.hs:13:13: error: in v tc141.hs:15:18: error: - • Couldn't match expected type ‘a2’ with actual type ‘p’ - ‘a2’ is a rigid type variable bound by + • Couldn't match expected type ‘a1’ with actual type ‘p1’ + ‘a1’ is a rigid type variable bound by the type signature for: - v :: forall a2. a2 + v :: forall a1. a1 at tc141.hs:14:14-19 - ‘p’ is a rigid type variable bound by - the inferred type of g :: a -> p -> a1 + ‘p1’ is a rigid type variable bound by + the inferred type of g :: p -> p1 -> a at tc141.hs:(13,1)-(16,13) • In the expression: b In an equation for ‘v’: v = b @@ -53,6 +53,6 @@ tc141.hs:15:18: error: v = b in v • Relevant bindings include - v :: a2 (bound at tc141.hs:15:14) - b :: p (bound at tc141.hs:13:5) - g :: a -> p -> a1 (bound at tc141.hs:13:1) + v :: a1 (bound at tc141.hs:15:14) + b :: p1 (bound at tc141.hs:13:5) + g :: p -> p1 -> a (bound at tc141.hs:13:1) diff --git a/testsuite/tests/typecheck/should_fail/T5689.stderr b/testsuite/tests/typecheck/should_fail/T5689.stderr index 2c7eaa87d4..5385f578b1 100644 --- a/testsuite/tests/typecheck/should_fail/T5689.stderr +++ b/testsuite/tests/typecheck/should_fail/T5689.stderr @@ -1,10 +1,6 @@ -T5689.hs:10:36: error: - • Couldn't match expected type ‘Bool’ with actual type ‘t’ - • In the expression: v - In the expression: if v then False else True - In the second argument of ‘writeIORef’, namely - ‘(\ v -> if v then False else True)’ - • Relevant bindings include - v :: t (bound at T5689.hs:10:28) - r :: IORef (t -> t) (bound at T5689.hs:7:14) +T5689.hs:15:23: error: + • No instance for (Num Bool) arising from the literal ‘1234’ + • In the first argument of ‘c’, namely ‘1234’ + In the second argument of ‘($)’, namely ‘c 1234’ + In a stmt of a 'do' block: print $ c 1234 diff --git a/testsuite/tests/typecheck/should_fail/T5691.stderr b/testsuite/tests/typecheck/should_fail/T5691.stderr index ad5c7e452f..d06a4f43a8 100644 --- a/testsuite/tests/typecheck/should_fail/T5691.stderr +++ b/testsuite/tests/typecheck/should_fail/T5691.stderr @@ -1,13 +1,4 @@ -T5691.hs:14:9: error: - • Couldn't match type ‘p’ with ‘PrintRuleInterp’ - Expected type: PrintRuleInterp a - Actual type: p a - • When checking that the pattern signature: p a - fits the type of its context: PrintRuleInterp a - In the pattern: f :: p a - In an equation for ‘test’: test (f :: p a) = MkPRI $ printRule_ f - T5691.hs:24:10: error: • No instance for (Alternative RecDecParser) arising from the superclasses of an instance declaration |