diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Errors/Ppr.hs | 11 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Errors/Types.hs | 16 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/App.hs | 21 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 14 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Equality.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 1 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 211 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 1 |
8 files changed, 266 insertions, 14 deletions
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 5cc8ab5f64..94f4d7b7df 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -1315,6 +1315,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 "Visibilities of forall-bound variables are not compatible") 2 $ + vcat + [ text "Expected:" <+> ppr exp + , text " Actual:" <+> ppr act ] TcRnCapturedTermName tv_name shadowed_term_names -> mkSimpleDecorated $ @@ -2311,7 +2317,8 @@ instance Diagnostic TcRnMessage where -> ErrorWithoutFlag TcRnInterfaceError err -> interfaceErrorReason err - + TcRnIncompatibleForallVisibility{} + -> ErrorWithoutFlag diagnosticHints = \case TcRnUnknownMessage m @@ -2913,6 +2920,8 @@ instance Diagnostic TcRnMessage where -> [SuggestAddTypeSignatures UnnamedBinding] TcRnInterfaceError reason -> interfaceErrorHints reason + TcRnIncompatibleForallVisibility{} + -> noHints diagnosticCode = constructorCode diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index 38615d0f0d..e80aaae161 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -3804,6 +3804,22 @@ data TcRnMessage where TcRnTypeSynonymCycle :: !TySynCycleTyCons -- ^ The tycons involved in the cycle -> TcRnMessage + {-| TcRnIncompatibleForallVisibility is an error that occurs when + the expected and actual types contain forall-bound variables + that have incompatible visibilities. + + Example: + type family Invis :: Type -> forall a. a + type family Vis :: Type -> forall a -> a + type instance Vis = Invis -- Bad instance + + Test cases: T18863a VisFlag1 VisFlag1_ql VisFlag2 VisFlag3 VisFlag4 VisFlag5 + -} + TcRnIncompatibleForallVisibility + :: TcType + -> TcType + -> TcRnMessage + deriving Generic -- | Things forbidden in @type data@ declarations. diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 818ec4e991..4bfcf3128a 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -352,6 +352,11 @@ tcApp rn_expr exp_res_ty = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $ thing_inside + -- QL may have instantiated some delta variables to polytypes. + -- Zonk before we call checkEqForallVis (and possibly tcSubTypeDS), + -- as those functions do not expect polytypes inside unification variables. + ; app_res_rho <- zonkQuickLook do_ql app_res_rho + -- Match up app_res_rho: the result type of rn_expr -- with exp_res_ty: the expected result type ; do_ds <- xoptM LangExt.DeepSubsumption @@ -368,10 +373,14 @@ tcApp rn_expr exp_res_ty -- Even though both app_res_rho and exp_res_ty are rho-types, -- they may have nested polymorphism, so if deep subsumption -- is on we must call tcSubType. - -- 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 - ; tcSubTypeDS rn_expr app_res_rho exp_res_ty } + tcSubTypeDS rn_expr app_res_rho exp_res_ty + + -- See Note [Use sites of checkEqForallVis] + -- This particular call is commented out because we do not have + -- visible forall in types of terms yet (#281), so it is a no-op. + -- ; case exp_res_ty of + -- Check res_ty -> checkEqForallVis app_res_rho res_ty + -- Infer _ -> return () -- Typecheck the value arguments ; tc_args <- tcValArgs do_ql inst_args @@ -1041,14 +1050,14 @@ qlUnify delta ty1 ty2 | -- See Note [Actual unification in qlUnify] let ty2_tvs = shallowTyCoVarsOfType ty2 , not (ty2_tvs `intersectsVarSet` bvs2) - -- Can't instantiate a delta-varto a forall-bound variable + -- Can't instantiate a delta-var to a forall-bound variable , Just ty2 <- occCheckExpand [kappa] ty2 -- Passes the occurs check = do { let ty2_kind = typeKind ty2 kappa_kind = tyVarKind kappa ; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see Note [Actual unification in qlUnify] - + ; checkEqForallVis ty2_kind kappa_kind -- See Note [Use sites of checkEqForallVis] ; 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 9e8375b47d..4ab6147081 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -1930,13 +1930,16 @@ checkExpectedKind hs_ty ty act_kind exp_kind ; let res_ty = ty `mkAppTys` new_args - ; if act_kind' `tcEqType` exp_kind + ; res_ty' <- + 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 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind , ppr exp_kind , ppr co_k ]) - ; return (res_ty `mkCastTy` co_k) } } + ; return (res_ty `mkCastTy` co_k) } + ; checkEqForallVis act_kind' exp_kind -- See Note [Use sites of checkEqForallVis] + ; return res_ty' } where -- We need to make sure that both kinds have the same number of implicit -- foralls out front. If the actual kind has more, instantiate accordingly. @@ -2551,7 +2554,8 @@ kcCheckDeclHeader_sig sig_kind name flav ; case ctx_k of AnyKind -> return () -- No signature _ -> do { res_ki <- newExpectedKind ctx_k - ; discardResult (unifyKind Nothing sig_res_kind' res_ki) } + ; discardResult (unifyKind Nothing sig_res_kind' res_ki) + ; checkEqForallVis sig_res_kind' res_ki } -- See Note [Use sites of checkEqForallVis] -- Add more binders for data/newtype, so the result kind has no arrows -- See Note [Datatype return kinds] @@ -2662,7 +2666,8 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside tc_hs_bndr (KindedTyVar _ _ (L _ hs_nm) lhs_kind) expected_kind = do { sig_kind <- tcLHsKindSig (TyVarBndrKindCtxt hs_nm) lhs_kind ; discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] - unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind } + unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind + ; checkEqForallVis sig_kind expected_kind } -- See Note [Use sites of checkEqForallVis] substTyConBinderX :: Subst -> TyConBinder -> (Subst, TyConBinder) substTyConBinderX subst (Bndr tv vis) @@ -3288,6 +3293,7 @@ bindExplicitTKBndrsX skol_mode@(SM { sm_parent = check_parent, sm_kind = ctxt_ki -- This unify rejects: -- class C (m :: * -> *) where -- type F (m :: *) = ... + ; checkEqForallVis kind (tyVarKind tv) -- See Note [Use sites of checkEqForallVis] ; return tv } | otherwise diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs index 2a76792790..6614dbdc51 100644 --- a/compiler/GHC/Tc/Solver/Equality.hs +++ b/compiler/GHC/Tc/Solver/Equality.hs @@ -216,9 +216,8 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _ = canTyConApp 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/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index caae46ce36..6a5b7230bc 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -922,6 +922,7 @@ tcDataFamInstHeader mb_clsinfo skol_info fam_tc hs_outer_bndrs fixity -- is none) ; let hs_lhs = nlHsTyConApp NotPromoted fixity (getName fam_tc) hs_pats ; _ <- unifyKind (Just . HsTypeRnThing $ unLoc hs_lhs) lhs_applied_kind res_kind + ; checkEqForallVis lhs_applied_kind res_kind -- See Note [Use sites of checkEqForallVis] ; traceTc "tcDataFamInstHeader" $ vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind, ppr m_ksig] diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 873ff2979a..1bf4121501 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -68,6 +68,10 @@ module GHC.Tc.Utils.TcMType ( inferResultToType, ensureMonoType, promoteTcType, -------------------------------- + -- Visibility flag check + tcEqForallVis, checkEqForallVis, + + -------------------------------- -- Zonking and tidying zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins, zonkTidyFRRInfos, @@ -606,6 +610,213 @@ tc_infer mb_frr tc_check {- ********************************************************************* * * + Visibility flag check +* * +********************************************************************* -} + +-- Check if two presumably equal types actually differ in the visibility +-- of their foralls. Example (from #18863): +-- +-- type IDa :: forall i -> i -> Type +-- data IDa :: forall i. i -> Type +-- +-- Report TcRnIncompatibleForallVisibility if the visibilities differ, +-- as in the example above. +-- +-- See Note [Presumably equal types] and Note [Use sites of checkEqForallVis] +checkEqForallVis :: TcType -> TcType -> TcM () +checkEqForallVis ty1 ty2 = + unless (tcEqForallVis ty1 ty2) $ + addErr $ TcRnIncompatibleForallVisibility ty1 ty2 + +-- Structurally match two presumably equal types, checking that all pairs of +-- foralls have equal visibilities. +-- +-- See Note [Presumably equal types] +tcEqForallVis :: Type -> Type -> Bool +tcEqForallVis = matchUpForAllTyFlags eqForAllVis + -- This is the only use of matchUpForAllTyFlags at the moment. + +-- Structurally match two presumably equal types, checking that all pairs of +-- forall visibility flags (ForAllTyFlag) satisfy a predicate. +-- +-- For example, given the types +-- ty1 = forall a1. Bool -> forall b1. ... +-- ty2 = forall a2. Bool -> forall b2 -> ... +-- We have +-- matchUpForAllTyFlags f ty1 ty2 = +-- f Specified Specified && -- from (a1, a2) +-- f Specified Required -- from (b1, b2) +-- +-- Metavariables are of no interest to us: they stand for monotypes, so there +-- are no forall flags to be found. We do not look through metavariables. +-- +-- See Note [Presumably equal types] +matchUpForAllTyFlags + :: (ForAllTyFlag -> ForAllTyFlag -> Bool) + -> TcType -- actual + -> TcType -- expected + -> Bool +matchUpForAllTyFlags zip_flags actual expected = + go actual expected True + where + go :: TcType -> TcType -> Bool -> Bool + -- See Note [Comparing nullary type synonyms] in GHC.Core.Type + go (TyConApp tc1 []) (TyConApp tc2 []) cont | tc1 == tc2 = cont + + go t1 t2 cont | Just t1' <- coreView t1 = go t1' t2 cont + go t1 t2 cont | Just t2' <- coreView t2 = go t1 t2' cont + + go (LitTy lit1) (LitTy lit2) cont + | lit1 /= lit2 = True -- See Note [Presumably equal types] + | otherwise = cont + + go (ForAllTy (Bndr tv1 vis1) ty1) (ForAllTy (Bndr tv2 vis2) ty2) cont + = go (varType tv1) (varType tv2) $ + go ty1 ty2 $ + zip_flags vis1 vis2 && cont + + go (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2) cont = + go arg1 arg2 $ go res1 res2 $ go w1 w2 $ cont + go (AppTy s1 t1) (AppTy s2 t2) cont = + go s1 s2 $ go t1 t2 $ cont + go (TyConApp tc1 ts1) (TyConApp tc2 ts2) cont + | tc1 /= tc2 = True -- See Note [Presumably equal types] + | otherwise = gos ts1 ts2 cont + + go (CastTy t1 _) t2 cont = go t1 t2 cont + go t1 (CastTy t2 _) cont = go t1 t2 cont + go _ _ cont = cont + + gos (t1:ts1) (t2:ts2) cont = gos ts1 ts2 $ go t1 t2 cont + gos [] [] cont = cont + gos _ _ _ = True -- See Note [Presumably equal types] + +{- Note [Presumably equal types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In matchUpForAllTyFlags (and by extension tcEqForallVis, checkEqForallVis) +we assume that there is always a separate (possibly subsequent) check for + t1 `eqType` t2 +eqType defines the equality relation that we are checking, but the actual +check may be performed by tcEqType or uType (unifyType/unifyKind). + +So `matchUpForAllTyFlags` should return True (i.e. "no problem") if the types +appear to differ. Examples: +* t1 is a unification variable and t2 is Int. + Later they will be unified -- no problems here! +* t1 is Int and t2 is Bool. + Later that will cause an error -- and it's bad for `checkEqForallVis` + to complain instead about mismatched visibilities. + +Note carefully that foralls can't hide inside unification variables +(unification variables stand for monotypes) so there is no danger of +missing a visiblitly mismatch with + alpha ~ (forall a -> blah) +where alpha is subsequently unified with (forall a. blah). +That latter unification can't happen. Quick Look does use unification variables +(so called "instantiation variables") but they are short lived. + +To reiterate, the ideal scenario is that `matchUpForAllTyFlags` returns True +when (ty1 /= ty2). In practice, however, it would make the check more +complicated and expensive. For instance, we'd have to maintain a RnEnv2 +to check type variables for equality. To make our lives easier, we follow +this principle on a best-effort basis. The worst case scenario is that +we report a less helpful error message. +-} + +{- Note [Use sites of checkEqForallVis] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The calls to checkEqForallVis must be carefully placed to cover all cases +but at the same time not incur the performance cost of excessive checking. + +Here we list all use sites of checkEqForallVis and examples of code covered +by that particular call. First, some helper definitions used in the examples: + + type family InvisF :: Type -> forall a. a + type family VisF :: Type -> forall a -> a + + 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 _ = () + +With those definitions in mind, here are the examples of code +for each call to checkEqForallVis: + +1. The call in GHC.Tc.Gen.HsType.checkExpectedKind + 1a) + Used when kind-checking type family instances (test: VisFlag2) + type instance VisF = InvisF + type instance InvisF = VisF + Here we try to unify the kinds of VisF and InvisF: + (Type -> forall a -> a) ~ (Type -> forall a. a) + 1b) + Used when kind-checking type applications (test: VisFlag1) + bad_tyapp :: () + bad_tyapp = f @V MkV + Here we use type applications to instantiatie hk := V (where hk is a type parameter of f), + therefore we unify their kinds + (forall j. j -> Type) ~ (forall k -> k -> Type) + +2. The call in GHC.Tc.Gen.App.qlUnify + Used when kind-checking Quick Look instantiations (test: VisFlag1_ql) + {-# LANGUAGE ImpredicativeTypes #-} + bad_infer :: () + bad_infer = f MkV + Here Quick Look tries to instantiate hk := V (where hk is a type parameter of f), + therefore we unify their kinds + (forall j. j -> Type) ~ (forall k -> k -> Type) + +3. The call in GHC.Tc.Utils.Unify.uUnfilledVar2 + Used when kind-checking inferred type variable instantiations (test: VisFlag1) + bad_infer :: () + bad_infer = f MkV + Here the unifier tries to fill in hk := V (where hk is a type parameter of f), + therefore we unify their kinds + (forall j. j -> Type) ~ (forall k -> k -> Type) + +4. The call in GHC.Tc.Gen.HsType.kcCheckDeclHeader_sig + Used when checking the result kind annotation + in type declarations with standalone kind signatures (test: T18863a) + type IDa :: forall i -> i -> Type + data IDa :: forall i. i -> Type + Here we unify the inline kind signature with the SAKS + (forall i -> i -> Type) ~ (forall i. i -> Type) + +5. The call in GHC.Tc.Gen.HsType.matchUpSigWithDecl + Used when checking kind annotations on type parameters + in type declarations with standalone kind signatures (test: VisFlag4) + type C :: (forall k -> k -> k) -> Constraint + class C (hk :: forall k. k -> k) where + Here we unify the inline kind signature on hk with the relevant + part of the SAKS + (forall k -> k -> k) ~ (forall k. k -> k) + +6. The call in GHC.Tc.Gen.HsType.bindExplicitTKBndrsX + Used when checking kind annotations on type parameters + of associated type families (test: VisFlag3) + class C (hk :: forall k. k -> k) where + type F (hk :: forall k -> k -> k) + Here we unify the kinds given to hk in F and C + (forall k. k -> k) ~ (forall k -> k -> k) + +7. The call in GHC.Tc.TyCl.Instance.tcDataFamInstHeader + Used when checking the result kind annotation + of data family instances (test: VisFlag5) + data family D a :: (forall i -> i -> i) -> Type + data instance D Int :: (forall i. i -> i) -> Type + Here we unify the result kinds in the data family header + and the data instance + ((forall i -> i -> i) -> Type) ~ ((forall i. i -> i) -> Type) + +8. The call in GHC.Tc.Gen.App.tcApp (commented out) + The commented out call in tcApp marks the spot where we should + perform the check when we implement visible forall in terms (#281). +-} + +{- ********************************************************************* +* * Promoting types * * ********************************************************************* -} diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index fc5728cc81..2d8e70ff64 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -2080,6 +2080,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 then not_ok_so_defer else do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1) + ; checkEqForallVis (typeKind ty2) (tyVarKind tv1) -- See Note [Use sites of checkEqForallVis] ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) |