From c955a514f033a12f6d0ab0fbacec3e18a5757ab5 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Sat, 14 Jul 2018 16:02:13 -0400 Subject: Remove decideKindGeneralisationPlan TypeInType came with a new function: decideKindGeneralisationPlan. This type-level counterpart to the term-level decideGeneralisationPlan chose whether or not a kind should be generalized. The thinking was that if `let` should not be generalized, then kinds shouldn't either (under the same circumstances around -XMonoLocalBinds). However, this is too conservative -- the situation described in the motivation for "let should be be generalized" does not occur in types. This commit thus removes decideKindGeneralisationPlan, always generalizing. One consequence is that tc_hs_sig_type_and_gen no longer calls solveEqualities, which reports all unsolved constraints, instead relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect of this is that reporing kind errors gets delayed more frequently. This seems to be a net benefit in error reporting; often, alongside a kind error, the type error is now reported (and users might find type errors easier to understand). Some of these errors ended up at the top level, where it was discovered that the GlobalRdrEnv containing the definitions in the local module was not in the TcGblEnv, and thus errors were reported with qualified names unnecessarily. This commit rejiggers some of the logic around captureTopConstraints accordingly. One error message (typecheck/should_fail/T1633) is a regression, mentioning the name of a default method. However, that problem is already reported as #10087, its solution is far from clear, and so I'm not addressing it here. This commit fixes #15141. As it's an internal refactor, there is no concrete test case for it. Along the way, we no longer need the hsib_closed field of HsImplicitBndrs (it was used only in decideKindGeneralisationPlan) and so it's been removed, simplifying the datatype structure. Along the way, I removed code in the validity checker that looks at coercions. This isn't related to this patch, really (though it was, at one point), but it's an improvement, so I kept it. This updates the haddock submodule. --- .../tests/dependent/should_compile/T14066h.hs | 11 ++++++++++ testsuite/tests/dependent/should_compile/all.T | 1 + .../tests/dependent/should_fail/DepFail1.stderr | 22 ++++++++++++++++---- .../tests/dependent/should_fail/T13895.stderr | 24 ++++++++++++++++++++++ .../tests/dependent/should_fail/T14066.stderr | 6 ++++-- .../tests/dependent/should_fail/T14066e.stderr | 11 +++++++++- testsuite/tests/dependent/should_fail/T14066h.hs | 11 ---------- .../tests/dependent/should_fail/T14066h.stderr | 16 --------------- testsuite/tests/dependent/should_fail/all.T | 1 - 9 files changed, 68 insertions(+), 35 deletions(-) create mode 100644 testsuite/tests/dependent/should_compile/T14066h.hs delete mode 100644 testsuite/tests/dependent/should_fail/T14066h.hs delete mode 100644 testsuite/tests/dependent/should_fail/T14066h.stderr (limited to 'testsuite/tests/dependent') diff --git a/testsuite/tests/dependent/should_compile/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs new file mode 100644 index 0000000000..df3db1c15d --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14066h.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-} + +module T14066h where + +import Data.Proxy + +f :: forall b. b -> (Proxy Int, Proxy Maybe) +f x = (fst y :: Proxy Int, fst y :: Proxy Maybe) + where + y :: (Proxy a, b) -- this generalizes over the kind of a + y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index 4e096c1f71..418fba2d85 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -53,3 +53,4 @@ test('T15264', normal, compile, ['']) test('DkNameRes', normal, compile, ['']) test('T15346', normal, compile, ['']) test('T15419', normal, compile, ['']) +test('T14066h', normal, compile, ['']) diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr index 630f010fa3..a8e64d4e0c 100644 --- a/testsuite/tests/dependent/should_fail/DepFail1.stderr +++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr @@ -2,11 +2,25 @@ DepFail1.hs:7:6: error: • Expecting one more argument to ‘Proxy Bool’ Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’ - • In the type signature: - z :: Proxy Bool + • In the type signature: z :: Proxy Bool + +DepFail1.hs:8:5: error: + • Couldn't match expected type ‘Proxy Bool’ + with actual type ‘Proxy k0 a1’ + • In the expression: P + In an equation for ‘z’: z = P DepFail1.hs:10:16: error: • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’ • In the second argument of ‘Proxy’, namely ‘Bool’ - In the type signature: - a :: Proxy Int Bool + In the type signature: a :: Proxy Int Bool + +DepFail1.hs:11:5: error: + • Couldn't match kind ‘*’ with ‘Int’ + When matching types + a0 :: Int + Bool :: * + Expected type: Proxy Int Bool + Actual type: Proxy Int a0 + • In the expression: P + In an equation for ‘a’: a = P diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr index 0ae1710bf0..3e8bef6858 100644 --- a/testsuite/tests/dependent/should_fail/T13895.stderr +++ b/testsuite/tests/dependent/should_fail/T13895.stderr @@ -1,4 +1,28 @@ +T13895.hs:8:14: error: + • Could not deduce (Typeable (t dict0)) + from the context: (Data a, Typeable (t dict)) + bound by the type signature for: + dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable + *) a (c :: * + -> *) (t :: forall k1. + Typeable + k1 => + k1 + -> *). + (Data a, Typeable (t dict)) => + (forall d. Data d => c (t dict1 d)) -> Maybe (c a) + at T13895.hs:(8,14)-(14,24) + The type variable ‘dict0’ is ambiguous + • In the ambiguity check for ‘dataCast1’ + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the type signature: + dataCast1 :: forall (a :: Type). + Data a => + forall (c :: Type -> Type) + (t :: forall (k :: Type). Typeable k => k -> Type). + Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) + T13895.hs:12:23: error: • Illegal constraint in a kind: Typeable k0 • In the first argument of ‘Typeable’, namely ‘t’ diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr index cd0142f5c1..e5179e510b 100644 --- a/testsuite/tests/dependent/should_fail/T14066.stderr +++ b/testsuite/tests/dependent/should_fail/T14066.stderr @@ -1,6 +1,6 @@ T14066.hs:15:59: error: - • Expected kind ‘k0’, but ‘b’ has kind ‘k’ + • Expected kind ‘k’, but ‘b’ has kind ‘k1’ • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: g :: forall k (b :: k). SameKind a b In the expression: @@ -8,4 +8,6 @@ T14066.hs:15:59: error: g :: forall k (b :: k). SameKind a b g = undefined in () - • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4) + • Relevant bindings include + x :: Proxy a (bound at T14066.hs:15:4) + f :: Proxy a -> () (bound at T14066.hs:15:1) diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index 504ca5a80e..193c74d193 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,6 +1,15 @@ T14066e.hs:13:59: error: - • Expected kind ‘c’, but ‘b'’ has kind ‘k0’ + • Couldn't match kind ‘k1’ with ‘*’ + ‘k1’ is a rigid type variable bound by + the type signature for: + j :: forall k k1 (c :: k1) (b :: k). + Proxy a -> Proxy b -> Proxy c -> Proxy b + at T14066e.hs:12:5-61 + When matching kinds + k :: * + c :: k1 + Expected kind ‘c’, but ‘b'’ has kind ‘k’ • In the first argument of ‘Proxy’, namely ‘(b' :: c')’ In an expression type signature: Proxy (b' :: c') In the expression: (p1 :: Proxy (b' :: c')) diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs deleted file mode 100644 index a20ae30958..0000000000 --- a/testsuite/tests/dependent/should_fail/T14066h.hs +++ /dev/null @@ -1,11 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables, PolyKinds, MonoLocalBinds #-} - -module T14066h where - -import Data.Proxy - -f :: forall b. b -> (Proxy Int, Proxy Maybe) -f x = (fst y :: Proxy Int, fst y :: Proxy Maybe) - where - y :: (Proxy a, b) -- MonoLocalBinds means this won't generalize over the kind of a - y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr deleted file mode 100644 index bfd33693b6..0000000000 --- a/testsuite/tests/dependent/should_fail/T14066h.stderr +++ /dev/null @@ -1,16 +0,0 @@ - -T14066h.hs:8:28: error: - • Couldn't match kind ‘* -> *’ with ‘*’ - When matching types - a0 :: * - Maybe :: * -> * - Expected type: Proxy Maybe - Actual type: Proxy a0 - • In the expression: fst y :: Proxy Maybe - In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe) - In an equation for ‘f’: - f x - = (fst y :: Proxy Int, fst y :: Proxy Maybe) - where - y :: (Proxy a, b) - y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 593b7787a1..0f7129020e 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, ['']) test('T14066e', normal, compile_fail, ['']) test('T14066f', normal, compile_fail, ['']) test('T14066g', normal, compile_fail, ['']) -test('T14066h', normal, compile_fail, ['']) test('T14845_fail1', normal, compile_fail, ['']) test('T14845_fail2', normal, compile_fail, ['']) test('InferDependency', normal, compile_fail, ['']) -- cgit v1.2.1