diff options
20 files changed, 89 insertions, 68 deletions
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 1d639d7f73..6cbe61b2b0 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -16,7 +16,7 @@ import GhcPrelude import TcRnTypes import TcRnMonad import TcMType -import TcUnify( occCheckForErrors, OccCheckResult(..) ) +import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) ) import TcEnv( tcInitTidyEnv ) import TcType import RnUnbound ( unknownNameSuggestions ) @@ -1632,7 +1632,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 , report ] - | OC_Occurs <- occ_check_expand + | MTVU_Occurs <- occ_check_expand -- We report an "occurs check" even for a ~ F t a, where F is a type -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it @@ -1657,10 +1657,10 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 ; mkErrorMsgFromCt ctxt ct $ mconcat [important main_msg, extra2, extra3, report] } - | OC_Bad <- occ_check_expand + | MTVU_Bad <- occ_check_expand = do { let msg = vcat [ text "Cannot instantiate unification variable" <+> quotes (ppr tv1) - , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2) + , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ] -- Unlike the other reports, this discards the old 'report_important' -- instead of augmenting it. This is because the details are not likely diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index d8b1edf492..cbf98d888c 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -31,7 +31,7 @@ module TcUnify ( matchActualFunTys, matchActualFunTysPart, matchExpectedFunKind, - metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..) + metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) ) where @@ -2115,43 +2115,43 @@ with (forall k. k->*) -} -data OccCheckResult a - = OC_OK a - | OC_Bad -- Forall or type family - | OC_Occurs +data MetaTyVarUpdateResult a + = MTVU_OK a + | MTVU_Bad -- Forall, predicate, or type family + | MTVU_Occurs -instance Functor OccCheckResult where +instance Functor MetaTyVarUpdateResult where fmap = liftM -instance Applicative OccCheckResult where - pure = OC_OK +instance Applicative MetaTyVarUpdateResult where + pure = MTVU_OK (<*>) = ap -instance Monad OccCheckResult where - OC_OK x >>= k = k x - OC_Bad >>= _ = OC_Bad - OC_Occurs >>= _ = OC_Occurs +instance Monad MetaTyVarUpdateResult where + MTVU_OK x >>= k = k x + MTVU_Bad >>= _ = MTVU_Bad + MTVU_Occurs >>= _ = MTVU_Occurs -occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult () --- Just for error-message generation; so we return OccCheckResult +occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () +-- Just for error-message generation; so we return MetaTyVarUpdateResult -- so the caller can report the right kind of error -- Check whether -- a) the given variable occurs in the given type. -- b) there is a forall in the type (unless we have -XImpredicativeTypes) occCheckForErrors dflags tv ty = case preCheck dflags True tv ty of - OC_OK _ -> OC_OK () - OC_Bad -> OC_Bad - OC_Occurs -> case occCheckExpand [tv] ty of - Nothing -> OC_Occurs - Just _ -> OC_OK () + MTVU_OK _ -> MTVU_OK () + MTVU_Bad -> MTVU_Bad + MTVU_Occurs -> case occCheckExpand [tv] ty of + Nothing -> MTVU_Occurs + Just _ -> MTVU_OK () ---------------- metaTyVarUpdateOK :: DynFlags -> TcTyVar -- tv :: k1 -> TcType -- ty :: k2 -> Maybe TcType -- possibly-expanded ty --- (metaTyFVarUpdateOK tv ty) +-- (metaTyVarUpdateOK tv ty) -- We are about to update the meta-tyvar tv with ty -- Check (a) that tv doesn't occur in ty (occurs check) -- (b) that ty does not have any foralls @@ -2178,17 +2178,18 @@ metaTyVarUpdateOK dflags tv ty = case preCheck dflags False tv ty of -- False <=> type families not ok -- See Note [Prevent unification with type families] - OC_OK _ -> Just ty - OC_Bad -> Nothing -- forall or type function - OC_Occurs -> occCheckExpand [tv] ty + MTVU_OK _ -> Just ty + MTVU_Bad -> Nothing -- forall, predicate, or type function + MTVU_Occurs -> occCheckExpand [tv] ty -preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult () +preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () -- A quick check for --- (a) a forall type (unless -XImpredivativeTypes) --- (b) a type family --- (c) an occurrence of the type variable (occurs check) +-- (a) a forall type (unless -XImpredicativeTypes) +-- (b) a predicate type (unless -XImpredicativeTypes) +-- (c) a type family +-- (d) an occurrence of the type variable (occurs check) -- --- For (a) and (b) we check only the top level of the type, NOT +-- For (a), (b), and (c) we check only the top level of the type, NOT -- inside the kinds of variables it mentions. But for (c) we do -- look in the kinds of course. @@ -2198,25 +2199,28 @@ preCheck dflags ty_fam_ok tv ty details = tcTyVarDetails tv impredicative_ok = canUnifyWithPolyType dflags details - ok :: OccCheckResult () - ok = OC_OK () + ok :: MetaTyVarUpdateResult () + ok = MTVU_OK () - fast_check :: TcType -> OccCheckResult () + fast_check :: TcType -> MetaTyVarUpdateResult () fast_check (TyVarTy tv') - | tv == tv' = OC_Occurs + | tv == tv' = MTVU_Occurs | otherwise = fast_check_occ (tyVarKind tv') -- See Note [Occurrence checking: look inside kinds] fast_check (TyConApp tc tys) - | bad_tc tc = OC_Bad + | bad_tc tc = MTVU_Bad | otherwise = mapM fast_check tys >> ok fast_check (LitTy {}) = ok - fast_check (FunTy _ a r) = fast_check a >> fast_check r + fast_check (FunTy{ft_af = af, ft_arg = a, ft_res = r}) + | InvisArg <- af + , not impredicative_ok = MTVU_Bad + | otherwise = fast_check a >> fast_check r fast_check (AppTy fun arg) = fast_check fun >> fast_check arg fast_check (CastTy ty co) = fast_check ty >> fast_check_co co fast_check (CoercionTy co) = fast_check_co co fast_check (ForAllTy (Bndr tv' _) ty) - | not impredicative_ok = OC_Bad + | not impredicative_ok = MTVU_Bad | tv == tv' = ok | otherwise = do { fast_check_occ (tyVarKind tv') ; fast_check_occ ty } @@ -2226,13 +2230,13 @@ preCheck dflags ty_fam_ok tv ty -- For kinds, we only do an occurs check; we do not worry -- about type families or foralls -- See Note [Checking for foralls] - fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs + fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs | otherwise = ok -- For coercions, we are only doing an occurs check here; -- no bother about impredicativity in coercions, as they're -- inferred - fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs + fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs | otherwise = ok bad_tc :: TyCon -> Bool diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs index c998f0967c..1188bf17d4 100644 --- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs +++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs @@ -34,7 +34,7 @@ fromInteger = Prelude.fromInteger insertStore = undefined schema = undefined -withTypeable = undefined +withTypeable _ _ = undefined throw# = undefined toDynamicST = undefined diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr index a170d29c46..56da989d37 100644 --- a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr +++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr @@ -12,4 +12,4 @@ Simplifier ticks exhausted simplifier non-termination has been judged acceptable. To see detailed counts use -ddump-simpl-stats - Total ticks: 140007 + Total ticks: 140086 diff --git a/testsuite/tests/ghci.debugger/scripts/print027.stdout b/testsuite/tests/ghci.debugger/scripts/print027.stdout index 3117eace87..eb5b363693 100644 --- a/testsuite/tests/ghci.debugger/scripts/print027.stdout +++ b/testsuite/tests/ghci.debugger/scripts/print027.stdout @@ -1,6 +1,6 @@ -+ = (_t1::Num a => a -> a -> a) -print = (_t2::Show a1 => a1 -> IO ()) -log = (_t3::Floating a2 => a2 -> a2) -head = (_t4::[a4] -> a4) -tail = (_t5::[a7] -> [a7]) -fst = (_t6::(a11, b) -> a11) ++ = (_t1::t1) +print = (_t2::t1) +log = (_t3::t1) +head = (_t4::[a] -> a) +tail = (_t5::[a1] -> [a1]) +fst = (_t6::(a2, b) -> a2) diff --git a/testsuite/tests/ghci/scripts/T12447.script b/testsuite/tests/ghci/scripts/T12447.script index 6003a43838..3bdd3f4b73 100644 --- a/testsuite/tests/ghci/scripts/T12447.script +++ b/testsuite/tests/ghci/scripts/T12447.script @@ -4,6 +4,6 @@ import Data.Typeable class Deferrable p where deferEither :: proxy p -> (p => r) -> Either String r -instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither = undefined +instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither _ _ = undefined :t deferEither @(_ ~ _) diff --git a/testsuite/tests/ghci/scripts/T14828.stdout b/testsuite/tests/ghci/scripts/T14828.stdout index 3ef2e602ec..9ccea0ceec 100644 --- a/testsuite/tests/ghci/scripts/T14828.stdout +++ b/testsuite/tests/ghci/scripts/T14828.stdout @@ -6,7 +6,7 @@ return :: Monad m => a -> m a return = (_t3::t1) pure :: Applicative f => a -> f a pure = (_t4::t1) -mempty = (_t5::Monoid a => a) -mappend = (_t6::Monoid a => a -> a -> a) +mempty = (_t5::t1) +mappend = (_t6::t1) foldl' = (_t7::t1) f = (_t8::t1) diff --git a/testsuite/tests/indexed-types/should_compile/T4358.hs b/testsuite/tests/indexed-types/should_compile/T4358.hs index 0c05576812..cb05a1c1aa 100644 --- a/testsuite/tests/indexed-types/should_compile/T4358.hs +++ b/testsuite/tests/indexed-types/should_compile/T4358.hs @@ -6,6 +6,6 @@ type family T a t2 :: forall a. ((T a ~ a) => a) -> a t2 = t - + t :: forall a. ((T a ~ a) => a) -> a -t = undefined +t _ = undefined diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr index 21af0d868a..e7448a9722 100644 --- a/testsuite/tests/indexed-types/should_fail/T5934.stderr +++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr @@ -1,7 +1,7 @@ T5934.hs:12:7: error: • Cannot instantiate unification variable ‘a0’ - with a type involving foralls: (forall s. GenST s) -> Int + with a type involving polytypes: (forall s. GenST s) -> Int GHC doesn't yet support impredicative polymorphism • In the expression: 0 In an equation for ‘run’: run = 0 diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr index a3b40c1222..4f5c5fcf29 100644 --- a/testsuite/tests/polykinds/T11142.stderr +++ b/testsuite/tests/polykinds/T11142.stderr @@ -7,7 +7,7 @@ T11142.hs:9:49: error: T11142.hs:10:7: error: • Cannot instantiate unification variable ‘a0’ - with a type involving foralls: + with a type involving polytypes: (forall k1 (a :: k1). SameKind a b) -> () GHC doesn't yet support impredicative polymorphism • In the expression: undefined diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs index 3eed83c657..d578be344e 100644 --- a/testsuite/tests/polykinds/T14270.hs +++ b/testsuite/tests/polykinds/T14270.hs @@ -76,7 +76,7 @@ splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b) splitApp (TrTyCon{}) = Nothing withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r -withTypeable = undefined +withTypeable _ _ = undefined eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) diff --git a/testsuite/tests/polykinds/T9569.hs b/testsuite/tests/polykinds/T9569.hs index 1b8bb68c75..634d742803 100644 --- a/testsuite/tests/polykinds/T9569.hs +++ b/testsuite/tests/polykinds/T9569.hs @@ -11,7 +11,7 @@ class Deferrable (c :: Constraint) where deferPair :: (Deferrable c1, Deferrable c2) => Proxy (c1,c2) -> ((c1,c2) => a) -> a -deferPair = undefined +deferPair _ _ = undefined instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where -- defer p f = deferPair p f -- Succeeds diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr index 32064a9c78..e4f1cc604d 100644 --- a/testsuite/tests/th/T11452.stderr +++ b/testsuite/tests/th/T11452.stderr @@ -8,7 +8,7 @@ T11452.hs:6:14: error: T11452.hs:6:14: error: • Cannot instantiate unification variable ‘p0’ - with a type involving foralls: forall a. a -> a + with a type involving polytypes: forall a. a -> a GHC doesn't yet support impredicative polymorphism • In the Template Haskell quotation [|| \ _ -> () ||] In the expression: [|| \ _ -> () ||] diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr index 05e926067f..efc87a1fc3 100644 --- a/testsuite/tests/typecheck/should_compile/T12427a.stderr +++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr @@ -3,7 +3,8 @@ T12427a.hs:17:29: error: • Couldn't match expected type ‘p’ with actual type ‘(forall b. [b] -> [b]) -> Int’ ‘p’ is a rigid type variable bound by - the inferred type of h11 :: T -> p at T12427a.hs:17:1-29 + the inferred type of h11 :: T -> p + at T12427a.hs:17:1-29 • In the expression: v In a case alternative: T1 _ v -> v In the expression: case y of { T1 _ v -> v } @@ -12,7 +13,7 @@ T12427a.hs:17:29: error: T12427a.hs:28:6: error: • Cannot instantiate unification variable ‘p0’ - with a type involving foralls: (forall b. [b] -> [b]) -> Int + with a type involving polytypes: (forall b. [b] -> [b]) -> Int GHC doesn't yet support impredicative polymorphism • In the pattern: T1 _ x1 In a pattern binding: T1 _ x1 = undefined diff --git a/testsuite/tests/typecheck/should_fail/T10194.stderr b/testsuite/tests/typecheck/should_fail/T10194.stderr index 7bc79b2e6f..aeaad79440 100644 --- a/testsuite/tests/typecheck/should_fail/T10194.stderr +++ b/testsuite/tests/typecheck/should_fail/T10194.stderr @@ -1,7 +1,7 @@ T10194.hs:7:8: error: - Cannot instantiate unification variable ‘b0’ - with a type involving foralls: X - GHC doesn't yet support impredicative polymorphism - In the expression: (.) - In an equation for ‘comp’: comp = (.) + • Cannot instantiate unification variable ‘b0’ + with a type involving polytypes: X + GHC doesn't yet support impredicative polymorphism + • In the expression: (.) + In an equation for ‘comp’: comp = (.) diff --git a/testsuite/tests/typecheck/should_fail/T11514.hs b/testsuite/tests/typecheck/should_fail/T11514.hs new file mode 100644 index 0000000000..f0dc07a22c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T11514.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE RankNTypes #-} + +module T11514 where + +foo :: forall a. (Show a => a -> a) -> () +foo = undefined diff --git a/testsuite/tests/typecheck/should_fail/T11514.stderr b/testsuite/tests/typecheck/should_fail/T11514.stderr new file mode 100644 index 0000000000..62acf15b73 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T11514.stderr @@ -0,0 +1,9 @@ + +T11514.hs:6:7: error: + • Cannot instantiate unification variable ‘a0’ + with a type involving polytypes: (Show a => a -> a) -> () + GHC doesn't yet support impredicative polymorphism + • In the expression: undefined + In an equation for ‘foo’: foo = undefined + • Relevant bindings include + foo :: (Show a => a -> a) -> () (bound at T11514.hs:6:1) diff --git a/testsuite/tests/typecheck/should_fail/T12563.stderr b/testsuite/tests/typecheck/should_fail/T12563.stderr index f32e99d1f0..e6619aa1da 100644 --- a/testsuite/tests/typecheck/should_fail/T12563.stderr +++ b/testsuite/tests/typecheck/should_fail/T12563.stderr @@ -1,7 +1,7 @@ T12563.hs:7:15: error: • Cannot instantiate unification variable ‘p0’ - with a type involving foralls: (forall a. f0 a) -> f0 r0 + with a type involving polytypes: (forall a. f0 a) -> f0 r0 GHC doesn't yet support impredicative polymorphism • In the first argument of ‘foo’, namely ‘g’ In the expression: foo g diff --git a/testsuite/tests/typecheck/should_fail/T12589.stderr b/testsuite/tests/typecheck/should_fail/T12589.stderr index 5e92f3af86..3f380e47a4 100644 --- a/testsuite/tests/typecheck/should_fail/T12589.stderr +++ b/testsuite/tests/typecheck/should_fail/T12589.stderr @@ -3,7 +3,7 @@ T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t T12589.hs:13:5: error: • Cannot instantiate unification variable ‘t0’ - with a type involving foralls: + with a type involving polytypes: (forall a. Bounded a => f0 a) -> h0 f0 xs0 GHC doesn't yet support impredicative polymorphism • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 6344d74c7a..d155ca0e8c 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -390,6 +390,7 @@ test('T11347', normal, compile_fail, ['']) test('T11356', normal, compile_fail, ['']) test('T11355', normal, compile_fail, ['']) test('T11464', normal, compile_fail, ['']) +test('T11514', normal, compile_fail, ['']) test('T11563', normal, compile_fail, ['']) test('T11541', normal, compile_fail, ['']) test('T11313', normal, compile_fail, ['']) |