diff options
32 files changed, 418 insertions, 45 deletions
diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs index 3629bc11a9..44ede9ca98 100644 --- a/compiler/GHC/Core/Map/Type.hs +++ b/compiler/GHC/Core/Map/Type.hs @@ -38,7 +38,6 @@ import GHC.Prelude import GHC.Core.Type import GHC.Core.Coercion import GHC.Core.TyCo.Rep -import GHC.Core.TyCo.Compare( eqForAllVis ) import GHC.Data.TrieMap import GHC.Data.FastString @@ -261,11 +260,8 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) = -> liftEquality (tc == tc') `andEq` gos env env' tys tys' (LitTy l, LitTy l') -> liftEquality (l == l') - (ForAllTy (Bndr tv vis) ty, ForAllTy (Bndr tv' vis') ty') - -> -- See Note [ForAllTy and type equality] in - -- GHC.Core.TyCo.Compare for why we use `eqForAllVis` here - liftEquality (vis `eqForAllVis` vis') `andEq` - go (D env (varType tv)) (D env' (varType tv')) `andEq` + (ForAllTy (Bndr tv _) ty, ForAllTy (Bndr tv' _) ty') + -> go (D env (varType tv)) (D env' (varType tv')) `andEq` go (D (extendCME env tv) ty) (D (extendCME env' tv') ty') (CoercionTy {}, CoercionTy {}) -> TEQ diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs index 4ef9d04eb8..a86c03d628 100644 --- a/compiler/GHC/Core/TyCo/Compare.hs +++ b/compiler/GHC/Core/TyCo/Compare.hs @@ -16,7 +16,7 @@ module GHC.Core.TyCo.Compare ( tcEqTyConApps, -- * Visiblity comparision - eqForAllVis, cmpForAllVis + eqForAllVis, ) where @@ -171,10 +171,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2 - go env (ForAllTy (Bndr tv1 vis1) ty1) - (ForAllTy (Bndr tv2 vis2) ty2) - = vis1 `eqForAllVis` vis2 - && (vis_only || go env (varType tv1) (varType tv2)) + go env (ForAllTy (Bndr tv1 _) ty1) + (ForAllTy (Bndr tv2 _) ty2) + = (vis_only || go env (varType tv1) (varType tv2)) && go (rnBndr2 env tv1 tv2) ty1 ty2 -- Make sure we handle all FunTy cases since falling through to the @@ -224,7 +223,6 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 {-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type]. - -- | Do these denote the same level of visibility? 'Required' -- arguments are visible, others are not. So this function -- equates 'Specified' and 'Inferred'. Used for printing. @@ -235,17 +233,6 @@ eqForAllVis Required Required = True eqForAllVis (Invisible _) (Invisible _) = True eqForAllVis _ _ = False --- | Do these denote the same level of visibility? 'Required' --- arguments are visible, others are not. So this function --- equates 'Specified' and 'Inferred'. Used for printing. -cmpForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Ordering --- See Note [ForAllTy and type equality] --- If you change this, see IMPORTANT NOTE in the above Note -cmpForAllVis Required Required = EQ -cmpForAllVis Required (Invisible {}) = LT -cmpForAllVis (Invisible _) Required = GT -cmpForAllVis (Invisible _) (Invisible _) = EQ - {- Note [ForAllTy and type equality] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -253,7 +240,7 @@ When we compare (ForAllTy (Bndr tv1 vis1) ty1) and (ForAllTy (Bndr tv2 vis2) ty2) what should we do about `vis1` vs `vis2`. -First, we always compare with `eqForAllVis` and `cmpForAllVis`. +First, we always compare with `eqForAllVis`. But what decision do we make? Should GHC type-check the following program (adapted from #15740)? @@ -513,10 +500,9 @@ nonDetCmpTypeX env orig_t1 orig_t2 = go env (TyVarTy tv1) (TyVarTy tv2) = liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2 - go env (ForAllTy (Bndr tv1 vis1) t1) (ForAllTy (Bndr tv2 vis2) t2) - = liftOrdering (vis1 `cmpForAllVis` vis2) - `thenCmpTy` go env (varType tv1) (varType tv2) - `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2 + go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2) + = go env (varType tv1) (varType tv2) + `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2 -- See Note [Equality on AppTys] go env (AppTy s1 t1) ty2 diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 112268097f..9cab90b834 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -1673,6 +1673,18 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 -- to be helpful since this is just an unimplemented feature. return (main_msg, []) + -- The kinds of 'tv1' and 'ty2' contain forall-bound variables that + -- differ in visibility (ForAllTyFlag). + | check_eq_result `cterHasProblem` cteForallKindVisDiff + = do + let + reason = ForallKindVisDiff tv1 ty2 + main_msg = + CannotUnifyVariable + { mismatchMsg = headline_msg + , cannotUnifyReason = reason } + return (main_msg, []) + | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 9880c13a9c..2469b772be 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -1226,6 +1226,12 @@ instance Diagnostic TcRnMessage where TcRnSectionWithoutParentheses expr -> mkSimpleDecorated $ hang (text "A section must be enclosed in parentheses") 2 (text "thus:" <+> (parens (ppr expr))) + TcRnIncompatibleForallVisibility act exp -> + mkSimpleDecorated $ + hang (text "Visibility of forall-bound variables is not compatible") 2 $ + vcat + [ text "Expected:" <+> ppr exp + , text " Actual:" <+> ppr act ] TcRnCapturedTermName tv_name shadowed_term_names -> mkSimpleDecorated $ @@ -1734,6 +1740,8 @@ instance Diagnostic TcRnMessage where -> ErrorWithoutFlag TcRnDuplicateMinimalSig{} -> ErrorWithoutFlag + TcRnIncompatibleForallVisibility{} + -> ErrorWithoutFlag diagnosticHints = \case TcRnUnknownMessage m @@ -2173,6 +2181,8 @@ instance Diagnostic TcRnMessage where -> noHints TcRnDuplicateMinimalSig{} -> noHints + TcRnIncompatibleForallVisibility{} + -> noHints diagnosticCode = constructorCode @@ -2970,6 +2980,10 @@ pprCannotUnifyVariableReason ctxt (DifferentTyVars tv_info) pprCannotUnifyVariableReason ctxt (RepresentationalEq tv_info mb_coercible_msg) = pprTyVarInfo ctxt tv_info $$ maybe empty pprCoercibleMsg mb_coercible_msg +pprCannotUnifyVariableReason _ (ForallKindVisDiff tv1 ty2) + = hang (text "Visibility of forall-bound variables in kinds differs") 2 $ + vcat [ ppr tv1 <+> text "::" <+> ppr (tyVarKind tv1) + , ppr ty2 <+> text "::" <+> ppr (typeKind ty2) ] pprMismatchMsg :: SolverReportErrCtxt -> MismatchMsg -> SDoc pprMismatchMsg ctxt diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index c1b8461839..5cb94bac68 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -2924,6 +2924,29 @@ data TcRnMessage where -} TcRnDuplicateMinimalSig :: LSig GhcPs -> LSig GhcPs -> [LSig GhcPs] -> TcRnMessage + {-| TcRnIncompatibleForallVisibility is an error that occurs when + the expected and actual types contain forall-bound variables + that have incompatible visibility or specificity. + + Example: + type family Invis :: Type -> forall a. a + type family Vis :: Type -> forall a -> a + type instance Vis = Invis -- Bad instance + + Test cases: + T18863a + T15079_fail_a + T22648a + T22648b + T22648c + T22648v + T22648v_ql + -} + TcRnIncompatibleForallVisibility + :: TcType + -> TcType + -> TcRnMessage + deriving Generic -- | Things forbidden in @type data@ declarations. @@ -3787,6 +3810,20 @@ data CannotUnifyVariableReason -- type Int, or with a 'TyVarTv'. | DifferentTyVars TyVarInfo | RepresentationalEq TyVarInfo (Maybe CoercibleMsg) + + -- | Can't unify a kind-polymorphic type variable with a type + -- due to visibility difference of forall-bound variables in their kinds. + -- + -- Example: + -- data V k (a :: k) = MkV + -- f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> () + -- bad_infer = f MkV + -- -- we want to unify hk := V + -- -- but hk :: forall j. j -> Type + -- -- V :: forall k -> k -> Type + -- + -- Test cases: T15079_fail_b T22648v + | ForallKindVisDiff TyVar Type deriving Generic -- | Report a mismatch error without any extra diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 06158cace3..d3388d0f24 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -362,6 +362,7 @@ tcApp rn_expr exp_res_ty -- so with simple subsumption we can just unify them -- No need to zonk; the unifier does that do { co <- unifyExpectedType rn_expr app_res_rho exp_res_ty + ; checkSubVis app_res_rho exp_res_ty ; return (mkWpCastN co) } else -- Deep subsumption @@ -371,6 +372,7 @@ tcApp rn_expr exp_res_ty -- Zonk app_res_rho first, because QL may have instantiated some -- delta variables to polytypes, and tcSubType doesn't expect that do { app_res_rho <- zonkQuickLook do_ql app_res_rho + ; checkSubVis app_res_rho exp_res_ty ; tcSubTypeDS rn_expr app_res_rho exp_res_ty } -- Typecheck the value arguments @@ -1052,7 +1054,7 @@ qlUnify delta ty1 ty2 kappa_kind = tyVarKind kappa ; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see Note [Actual unification in qlUnify] - + ; checkSubVis ty2_kind (Check kappa_kind) ; traceTc "qlUnify:update" $ vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind) 2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind) diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 222755f6c9..651193bb2b 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -1931,6 +1931,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind ; let res_ty = ty `mkAppTys` new_args + ; checkSubVis act_kind' (mkCheckExpType exp_kind) ; if act_kind' `tcEqType` exp_kind then return res_ty -- This is very common else do { co_k <- uType KindLevel origin act_kind' exp_kind @@ -2552,6 +2553,7 @@ kcCheckDeclHeader_sig sig_kind name flav ; case ctx_k of AnyKind -> return () -- No signature _ -> do { res_ki <- newExpectedKind ctx_k + ; checkSubVis res_ki (mkCheckExpType sig_res_kind') ; discardResult (unifyKind Nothing sig_res_kind' res_ki) } -- Add more binders for data/newtype, so the result kind has no arrows diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index ea2d95e80d..9dd55ede48 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -1095,9 +1095,8 @@ can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ = canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2 can_eq_nc' _rewritten _rdr_env _envs ev eq_rel - s1@(ForAllTy (Bndr _ vis1) _) _ - s2@(ForAllTy (Bndr _ vis2) _) _ - | vis1 `eqForAllVis` vis2 -- Note [ForAllTy and type equality] + s1@(ForAllTy _ _) _ + s2@(ForAllTy _ _) _ = can_eq_nc_forall ev eq_rel s1 s2 -- See Note [Canonicalising type applications] about why we require rewritten types diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 0623acd3d5..bad9f781a7 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -34,6 +34,7 @@ module GHC.Tc.Types.Constraint ( CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck, cteOK, cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble, + cteForallKindVisDiff, cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterRemoveProblem, cterHasOccursCheck, cterFromKind, @@ -452,12 +453,13 @@ cterHasNoProblem _ = False -- | An individual problem that might be logged in a 'CheckTyEqResult' newtype CheckTyEqProblem = CTEP Word8 -cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs :: CheckTyEqProblem +cteImpredicative, cteTypeFamily, cteInsolubleOccurs, cteSolubleOccurs, cteForallKindVisDiff :: CheckTyEqProblem cteImpredicative = CTEP (bit 0) -- forall or (=>) encountered cteTypeFamily = CTEP (bit 1) -- type family encountered cteInsolubleOccurs = CTEP (bit 2) -- occurs-check cteSolubleOccurs = CTEP (bit 3) -- occurs-check under a type function or in a coercion -- must be one bit to the left of cteInsolubleOccurs +cteForallKindVisDiff = CTEP (bit 4) -- differing visibility of forall-bound variables in the kind -- See also Note [Insoluble occurs check] in GHC.Tc.Errors cteProblem :: CheckTyEqProblem -> CheckTyEqResult @@ -521,7 +523,8 @@ instance Outputable CheckTyEqResult where all_bits = [ (cteImpredicative, "cteImpredicative") , (cteTypeFamily, "cteTypeFamily") , (cteInsolubleOccurs, "cteInsolubleOccurs") - , (cteSolubleOccurs, "cteSolubleOccurs") ] + , (cteSolubleOccurs, "cteSolubleOccurs") + , (cteForallKindVisDiff, "cteForallKindVisDiff") ] set_bits = [ text str | (bitmask, str) <- all_bits , cter `cterHasProblem` bitmask ] diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index d0afe71560..6e53b6dccb 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -67,6 +67,10 @@ module GHC.Tc.Utils.TcMType ( inferResultToType, ensureMonoType, promoteTcType, -------------------------------- + -- Visibility subsumption + tcSubVis, tcEqVis, checkSubVis, + + -------------------------------- -- Zonking and tidying zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins, zonkTidyFRRInfos, @@ -606,6 +610,79 @@ tc_infer mb_frr tc_check {- ********************************************************************* * * + Visibility subsumption +* * +********************************************************************* -} + +checkSubVis :: TcType -> ExpType -> TcM () +checkSubVis _ (Infer _) = return () +checkSubVis ty1 (Check ty2) = + unless (tcSubVis ty1 ty2) $ + addErr $ TcRnIncompatibleForallVisibility ty1 ty2 + +tcEqVis :: Type -> Type -> Bool +tcEqVis ty1 ty2 = + Semi.getAll (zipForAllTyFlags eq_vis ty1 ty2) + where + eq_vis :: ForAllTyFlag -> ForAllTyFlag -> Semi.All + eq_vis flag1 flag2 = Semi.All (flag1 == flag2) + +tcSubVis + :: Type -- actual + -> Type -- expected + -> Bool +tcSubVis actual expected = + Semi.getAll (zipForAllTyFlags sub_vis actual expected) + where + sub_vis :: ForAllTyFlag -> ForAllTyFlag -> Semi.All + sub_vis Specified Inferred = Semi.All True + sub_vis flag1 flag2 = Semi.All (flag1 == flag2) + +zipForAllTyFlags + :: forall m. Monoid m => + (ForAllTyFlag -> ForAllTyFlag -> m) + -> Type -- actual + -> Type -- expected + -> m +zipForAllTyFlags zip_flags actual expected = + go (typeKind actual) (typeKind expected) Semi.<> + go actual expected + where + go :: Type -> Type -> m + + -- See Note [Comparing nullary type synonyms] in GHC.Core.Type + go (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = mempty + + go t1 t2 | Just t1' <- coreView t1 = go t1' t2 + go t1 t2 | Just t2' <- coreView t2 = go t1 t2' + + go (ForAllTy (Bndr tv1 vis1) ty1) (ForAllTy (Bndr tv2 vis2) ty2) + = zip_flags vis1 vis2 + Semi.<> go (varType tv1) (varType tv2) + Semi.<> go ty1 ty2 + + go (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) = + go arg1 arg2 Semi.<> go res1 res2 Semi.<> go w1 w2 + + -- See Note [Equality on AppTys] in GHC.Core.Type + go (AppTy s1 t1) ty2 + | Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2 + = go s1 s2 Semi.<> go t1 t2 + go ty1 (AppTy s2 t2) + | Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1 + = go s1 s2 Semi.<> go t1 t2 + + go (TyConApp _ ts1) (TyConApp _ ts2) = gos ts1 ts2 + + go (CastTy t1 _) t2 = go t1 t2 + go t1 (CastTy t2 _) = go t1 t2 + go _ _ = mempty + + gos (t1:ts1) (t2:ts2) = go t1 t2 Semi.<> gos ts1 ts2 + gos _ _ = mempty + +{- ********************************************************************* +* * Promoting types * * ********************************************************************* -} diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index eea0ed95ef..8344d95389 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -21,6 +21,7 @@ module GHC.Tc.Utils.Unify ( unifyType, unifyKind, unifyExpectedType, uType, promoteTcType, swapOverTyVars, startSolvingByUnification, + tcSubVis, -------------------------------- -- Holes @@ -2636,12 +2637,13 @@ checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult -- case-analysis on 'lhs') -- * checkEqCanLHSFinish, which does not know the form of 'lhs' checkTypeEq lhs ty - = go ty + = go ty S.<> check_kind_vis (canEqLHSKind lhs) (typeKind ty) where impredicative = cteProblem cteImpredicative type_family = cteProblem cteTypeFamily insoluble_occurs = cteProblem cteInsolubleOccurs soluble_occurs = cteProblem cteSolubleOccurs + forall_kind_vis_diff = cteProblem cteForallKindVisDiff -- The GHCi runtime debugger does its type-matching with -- unification variables that can unify with a polytype @@ -2721,3 +2723,8 @@ checkTypeEq lhs ty | ghci_tv = \ _tc -> cteOK | otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<> (if isFamFreeTyCon tc then cteOK else type_family) + + check_kind_vis :: TcKind -> TcKind -> CheckTyEqResult + check_kind_vis k1 k2 + | tcEqVis k1 k2 = cteOK + | otherwise = forall_kind_vis_diff diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs index d7b57113ee..89d9a03066 100644 --- a/compiler/GHC/Types/Error/Codes.hs +++ b/compiler/GHC/Types/Error/Codes.hs @@ -321,6 +321,7 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "SkolemEscape" = 46956 GhcDiagnosticCode "DifferentTyVars" = 25897 GhcDiagnosticCode "RepresentationalEq" = 10283 + GhcDiagnosticCode "ForallKindVisDiff" = 11809 -- Typechecker/renamer diagnostic codes GhcDiagnosticCode "TcRnRedundantConstraints" = 30606 @@ -512,6 +513,7 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "TcRnUnexpectedDefaultSig" = 40700 GhcDiagnosticCode "TcRnBindInBootFile" = 11247 GhcDiagnosticCode "TcRnDuplicateMinimalSig" = 85346 + GhcDiagnosticCode "TcRnIncompatibleForallVisibility" = 25115 -- IllegalNewtypeReason GhcDiagnosticCode "DoesNotHaveSingleField" = 23517 diff --git a/testsuite/tests/dependent/should_compile/T11966.hs b/testsuite/tests/dependent/should_compile/T11966.hs index daad450f13..d1b7662a43 100644 --- a/testsuite/tests/dependent/should_compile/T11966.hs +++ b/testsuite/tests/dependent/should_compile/T11966.hs @@ -24,7 +24,7 @@ newtype HasDefault t = HasDefault t -- Interpretations data Expr k -data Record (f :: forall k. k -> Type) = +data Record (f :: forall {k}. k -> Type) = Record {rX :: Col f ('Column "x" 'PGInteger) ,rY :: Col f ('Column "y" ('Nullable 'PGInteger)) ,rZ :: Col f ('HasDefault 'PGText)} diff --git a/testsuite/tests/indexed-types/should_compile/T15740a.hs b/testsuite/tests/indexed-types/should_compile/T15740a.hs index f209e243c6..5b8881aa50 100644 --- a/testsuite/tests/indexed-types/should_compile/T15740a.hs +++ b/testsuite/tests/indexed-types/should_compile/T15740a.hs @@ -5,7 +5,7 @@ module T15740a where import Data.Kind import Data.Proxy -type family F2 :: forall k. k -> Type +type family F2 :: forall {k}. k -> Type -- This should succeed type instance F2 = Proxy diff --git a/testsuite/tests/saks/should_compile/saks032.hs b/testsuite/tests/saks/should_compile/saks032.hs index 612c66d8fc..ce33110341 100644 --- a/testsuite/tests/saks/should_compile/saks032.hs +++ b/testsuite/tests/saks/should_compile/saks032.hs @@ -4,11 +4,13 @@ module SAKS_032 where import Data.Kind -import Data.Proxy type Const :: Type -> forall k. k -> Type data Const a b = Const a +type Proxy :: forall k. k -> Type +data Proxy a = Proxy + type F :: Type -> Type -> forall k. k -> Type type family F a b :: forall k. k -> Type where F () () = Proxy diff --git a/testsuite/tests/saks/should_fail/T18863a.stderr b/testsuite/tests/saks/should_fail/T18863a.stderr index c36a102530..3116546dcf 100644 --- a/testsuite/tests/saks/should_fail/T18863a.stderr +++ b/testsuite/tests/saks/should_fail/T18863a.stderr @@ -1,5 +1,6 @@ -T18863a.hs:9:1: error: [GHC-83865] - • Couldn't match expected kind: forall i. i -> * - with actual kind: forall i -> i -> * +T18863a.hs:9:1: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall i -> i -> * + Actual: forall i. i -> * • In the data type declaration for ‘IDa’ diff --git a/testsuite/tests/typecheck/should_compile/T15079.hs b/testsuite/tests/typecheck/should_compile/T15079.hs index 22e86abc56..c20ada216e 100644 --- a/testsuite/tests/typecheck/should_compile/T15079.hs +++ b/testsuite/tests/typecheck/should_compile/T15079.hs @@ -15,7 +15,7 @@ import GHC.Exts (Any) infixl 4 :== -- | Heterogeneous Leibnizian equality. newtype (a :: j) :== (b :: k) - = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b } + = HRefl { hsubst :: forall (c :: forall {i :: Type}. i -> Type). c a -> c b } ----- @@ -29,9 +29,9 @@ coerce f = uncoerce . hsubst f . Coerce ----- -newtype Flay :: (forall (i :: Type). i -> i -> Type) +newtype Flay :: (forall {i :: Type}. i -> i -> Type) -> forall (j :: Type). j -> forall (k :: Type). k -> Type where - Flay :: forall (p :: forall (i :: Type). i -> i -> Type) + Flay :: forall (p :: forall {i :: Type}. i -> i -> Type) (j :: Type) (k :: Type) (a :: j) (b :: k). { unflay :: p a (MassageKind j b) } -> Flay p a b @@ -44,7 +44,7 @@ fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl ----- -newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int) +newtype Foo (f :: forall {a :: Type}. a -> Type) = MkFoo (f Int) data InferredProxy a = MkInferredProxy foo :: Foo InferredProxy diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs b/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs new file mode 100644 index 0000000000..7cec93872f --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15079_fail_a.hs @@ -0,0 +1,9 @@ +module T15079_fail_a where + +import Data.Kind (Type) + +newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int) +data InferredProxy a = MkInferredProxy + +foo :: Foo InferredProxy +foo = MkFoo MkInferredProxy
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr b/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr new file mode 100644 index 0000000000..83765d7f82 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15079_fail_a.stderr @@ -0,0 +1,7 @@ + +T15079_fail_a.hs:8:12: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall a. a -> * + Actual: forall {k}. k -> * + • In the first argument of ‘Foo’, namely ‘InferredProxy’ + In the type signature: foo :: Foo InferredProxy diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs b/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs new file mode 100644 index 0000000000..227839c7b9 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15079_fail_b.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE TypeFamilies #-} + +module T15079_fail_b where + +import Data.Kind (Type) +import Data.Void (Void) + +infixl 4 :== +-- | Heterogeneous Leibnizian equality. +newtype (a :: j) :== (b :: k) + = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b } + +newtype Coerce a = Coerce { uncoerce :: Starify a } + +type Starify :: k -> Type +type family Starify (a :: k) :: Type where + Starify (a :: Type) = a + Starify _ = Void + +coerce :: a :== b -> a -> b +coerce f = uncoerce . hsubst f . Coerce
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr b/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr new file mode 100644 index 0000000000..f99f557725 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15079_fail_b.stderr @@ -0,0 +1,11 @@ + +T15079_fail_b.hs:21:23: error: [GHC-11809] + • Couldn't match type ‘c0’ with ‘Coerce’ + Expected: c0 a -> Coerce b + Actual: c0 a -> c0 b + Visibility of forall-bound variables in kinds differs + c0 :: forall i. i -> * + Coerce :: forall {k}. k -> * + • In the first argument of ‘(.)’, namely ‘hsubst f’ + In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’ + In the expression: uncoerce . hsubst f . Coerce diff --git a/testsuite/tests/typecheck/should_fail/T22648a.hs b/testsuite/tests/typecheck/should_fail/T22648a.hs new file mode 100644 index 0000000000..72ac0b14af --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648a.hs @@ -0,0 +1,7 @@ +module T22648a where + +const_inf :: () -> forall {a} {b}. a -> b -> a +const_inf _ x _ = x + +const_spec :: () -> forall a b. a -> b -> a +const_spec = const_inf
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22648a.stderr b/testsuite/tests/typecheck/should_fail/T22648a.stderr new file mode 100644 index 0000000000..3f8eb41adc --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648a.stderr @@ -0,0 +1,7 @@ + +T22648a.hs:7:14: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: () -> forall a b. a -> b -> a + Actual: () -> forall {a} {b}. a -> b -> a + • In the expression: const_inf + In an equation for ‘const_spec’: const_spec = const_inf diff --git a/testsuite/tests/typecheck/should_fail/T22648b.hs b/testsuite/tests/typecheck/should_fail/T22648b.hs new file mode 100644 index 0000000000..5ec28af471 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648b.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE TypeFamilies #-} + +module T22648b where + +import Data.Kind (Type) + +type D1 :: forall {k1} {k2}. k1 -> k2 -> Type +data D1 a b + +type family F :: forall k1 k2. k1 -> k2 -> Type +type instance F = D1
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22648b.stderr b/testsuite/tests/typecheck/should_fail/T22648b.stderr new file mode 100644 index 0000000000..50d9c95c37 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648b.stderr @@ -0,0 +1,7 @@ + +T22648b.hs:11:19: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall k1 k2. k1 -> k2 -> * + Actual: forall {k1} {k2}. k1 -> k2 -> * + • In the type ‘D1’ + In the type instance declaration for ‘F’ diff --git a/testsuite/tests/typecheck/should_fail/T22648c.hs b/testsuite/tests/typecheck/should_fail/T22648c.hs new file mode 100644 index 0000000000..e81d97da0e --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648c.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE DataKinds #-} + +module T22648c where + +import GHC.TypeLits (Nat) +import Data.Kind (Type) + +-- 1. the (i :: Nat) parameter to avoid conflicting instances +-- 2. the (Type ->) parameter is to prevent instantiation of invisible variables + +type family Infer (i :: Nat) :: Type -> forall {a}. a +type family Invis (i :: Nat) :: Type -> forall a. a +type family Vis (i :: Nat) :: Type -> forall a -> a + +type instance Vis 1 = Invis 0 -- Bad +type instance Invis 2 = Vis 0 -- Bad + +type instance Vis 3 = Infer 0 -- Bad +type instance Infer 4 = Vis 0 -- Bad + +type instance Invis 5 = Infer 0 -- Bad +type instance Infer 6 = Invis 0 -- Ok
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T22648c.stderr b/testsuite/tests/typecheck/should_fail/T22648c.stderr new file mode 100644 index 0000000000..cb92ed89f0 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648c.stderr @@ -0,0 +1,35 @@ + +T22648c.hs:17:23: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: * -> forall a -> a + Actual: * -> forall a. a + • In the type ‘Invis 0’ + In the type instance declaration for ‘Vis’ + +T22648c.hs:18:25: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: * -> forall a. a + Actual: * -> forall a -> a + • In the type ‘Vis 0’ + In the type instance declaration for ‘Invis’ + +T22648c.hs:20:23: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: * -> forall a -> a + Actual: * -> forall {a}. a + • In the type ‘Infer 0’ + In the type instance declaration for ‘Vis’ + +T22648c.hs:21:25: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: * -> forall {a}. a + Actual: * -> forall a -> a + • In the type ‘Vis 0’ + In the type instance declaration for ‘Infer’ + +T22648c.hs:23:25: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: * -> forall a. a + Actual: * -> forall {a}. a + • In the type ‘Infer 0’ + In the type instance declaration for ‘Invis’ diff --git a/testsuite/tests/typecheck/should_fail/T22648v.hs b/testsuite/tests/typecheck/should_fail/T22648v.hs new file mode 100644 index 0000000000..1de83211f7 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648v.hs @@ -0,0 +1,18 @@ +module T22648v where + +import Data.Kind (Type) + +type V :: forall k -> k -> Type +data V k (a :: k) = MkV + +f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> () +f _ = () + +bad_tyapp :: () +bad_tyapp = f @V MkV + +bad_wild :: () +bad_wild = f @_ MkV + +bad_infer :: () +bad_infer = f MkV diff --git a/testsuite/tests/typecheck/should_fail/T22648v.stderr b/testsuite/tests/typecheck/should_fail/T22648v.stderr new file mode 100644 index 0000000000..7ff1f6ed25 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648v.stderr @@ -0,0 +1,26 @@ + +T22648v.hs:12:16: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall j. j -> * + Actual: forall k -> k -> * + • In the type ‘V’ + In the expression: f @V MkV + In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV + +T22648v.hs:15:15: error: [GHC-91028] + • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’ + Cannot instantiate unification variable ‘k0’ + with a kind involving polytypes: forall j. j -> * + • In the expression: f @_ MkV + In an equation for ‘bad_wild’: bad_wild = f @_ MkV + +T22648v.hs:18:15: error: [GHC-11809] + • Couldn't match type ‘hk0’ with ‘V’ + Expected: hk0 a0 + Actual: V k1 a0 + Visibility of forall-bound variables in kinds differs + hk0 :: forall j. j -> * + V :: forall k -> k -> * + • In the first argument of ‘f’, namely ‘MkV’ + In the expression: f MkV + In an equation for ‘bad_infer’: bad_infer = f MkV diff --git a/testsuite/tests/typecheck/should_fail/T22648v_ql.hs b/testsuite/tests/typecheck/should_fail/T22648v_ql.hs new file mode 100644 index 0000000000..3e3107f92c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648v_ql.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE ImpredicativeTypes #-} + +module T22648v_ql where + +import Data.Kind (Type) + +type V :: forall k -> k -> Type +data V k (a :: k) = MkV + +f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> () +f _ = () + +bad_tyapp :: () +bad_tyapp = f @V MkV + +bad_wild :: () +bad_wild = f @_ MkV + +bad_infer :: () +bad_infer = f MkV diff --git a/testsuite/tests/typecheck/should_fail/T22648v_ql.stderr b/testsuite/tests/typecheck/should_fail/T22648v_ql.stderr new file mode 100644 index 0000000000..1283f0107b --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T22648v_ql.stderr @@ -0,0 +1,23 @@ + +T22648v_ql.hs:14:16: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall j. j -> * + Actual: forall k -> k -> * + • In the type ‘V’ + In the expression: f @V MkV + In an equation for ‘bad_tyapp’: bad_tyapp = f @V MkV + +T22648v_ql.hs:17:15: error: [GHC-91028] + • Expected kind ‘forall j. j -> *’, but ‘_’ has kind ‘k0’ + Cannot instantiate unification variable ‘k0’ + with a kind involving polytypes: forall j. j -> * + • In the expression: f @_ MkV + In an equation for ‘bad_wild’: bad_wild = f @_ MkV + +T22648v_ql.hs:20:15: error: [GHC-25115] + • Visibility of forall-bound variables is not compatible + Expected: forall j. j -> * + Actual: forall k -> k -> * + • In the first argument of ‘f’, namely ‘MkV’ + In the expression: f MkV + In an equation for ‘bad_infer’: bad_infer = f MkV diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index a7e9f6a678..cd2758ad17 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -667,3 +667,10 @@ test('T22570', normal, compile_fail, ['']) test('T22645', normal, compile_fail, ['']) test('T20666', normal, compile_fail, ['']) test('T20666a', normal, compile_fail, ['']) +test('T22648a', normal, compile_fail, ['']) +test('T22648b', normal, compile_fail, ['']) +test('T22648c', normal, compile_fail, ['']) +test('T22648v', normal, compile_fail, ['']) +test('T22648v_ql', normal, compile_fail, ['']) +test('T15079_fail_a', normal, compile_fail, ['']) +test('T15079_fail_b', normal, compile_fail, ['']) |