diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/GHC/Core/Map/Type.hs | 9 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCo/Compare.hs | 112 | ||||
| -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 | ||||
| -rw-r--r-- | compiler/GHC/Types/Error/Codes.hs | 1 |
11 files changed, 325 insertions, 77 deletions
diff --git a/compiler/GHC/Core/Map/Type.hs b/compiler/GHC/Core/Map/Type.hs index d94f97fb19..80595ce80e 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,9 @@ 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') + -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare + -> 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..564c38490f 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,11 +171,13 @@ 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 (rnBndr2 env tv1 tv2) ty1 ty2 + go env (ForAllTy (Bndr tv1 _) ty1) + (ForAllTy (Bndr tv2 _) ty2) + -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality] + = kinds_eq && go (rnBndr2 env tv1 tv2) ty1 ty2 + where + kinds_eq | vis_only = True + | otherwise = go env (varType tv1) (varType tv2) -- Make sure we handle all FunTy cases since falling through to the -- AppTy case means that tcSplitAppTyNoView_maybe may see an unzonked @@ -227,7 +229,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2 -- | 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. +-- equates 'Specified' and 'Inferred'. +-- +-- Used for printing and in tcEqForallVis. eqForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Bool -- See Note [ForAllTy and type equality] -- If you change this, see IMPORTANT NOTE in the above Note @@ -235,28 +239,41 @@ 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] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 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`. -But what decision do we make? - -Should GHC type-check the following program (adapted from #15740)? +what should we do about `vis1` vs `vis2`? + +An extensive discussion can be found at https://github.com/ghc-proposals/ghc-proposals/issues/558. +A short summary of our options and the currently implemented design are described below. + +One option is to take those flags into account and check (vis1==vis2). +But in Core, the visibilities of forall-bound variables have no meaning, +as type abstraction and type application are always explicit. +Going to great lengths to carry them around is counterproductive, +but not going far enough may lead to Core Lint errors (#22762). + +The other option (the one we take) is to ignore those flags. +Neither the name of a forall-bound variable nor its visibility flag +affect GHC's notion of type equality. + +That said, the visibilities of foralls do matter +a great deal in user-written programs. For example, if we unify tv := T, where + tv :: forall k. k -> Type + T :: forall k -> k -> Type +then the user cannot substitute `T Maybe` for `tv Maybe` in their program +by hand. They'd have to write `T (Type -> Type) Maybe` instead. +This entails a loss of referential transparency. We solve this issue by +checking the flags in the (source-language) type checker, not in the +(Core language) equality relation `eqType`. All checks of forall visibility +are listed in Note [Use sites of checkEqForallVis]. + +These checks use `eqForAllVis` to compare the `ForAllTyFlag`s. +But should we perhaps use (==) instead? +Do we only care about visibility (Required vs Invisible) +or do we also care about specificity (Specified vs Inferred)? +For example, should GHC type-check the following program (adapted from #15740)? {-# LANGUAGE PolyKinds, ... #-} data D a @@ -280,34 +297,15 @@ programs like the one above. Whether a kind variable binder ends up being specified or inferred can be somewhat subtle, however, especially for kinds that aren't explicitly written out in the source code (like in D above). -For now, we decide - - the specified/inferred status of an invisible type variable binder - does not affect GHC's notion of equality. - -That is, we have the following: - - -------------------------------------------------- - | Type 1 | Type 2 | Equal? | - --------------------|----------------------------- - | forall k. <...> | forall k. <...> | Yes | - | | forall {k}. <...> | Yes | - | | forall k -> <...> | No | - -------------------------------------------------- - | forall {k}. <...> | forall k. <...> | Yes | - | | forall {k}. <...> | Yes | - | | forall k -> <...> | No | - -------------------------------------------------- - | forall k -> <...> | forall k. <...> | No | - | | forall {k}. <...> | No | - | | forall k -> <...> | Yes | - -------------------------------------------------- - -IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry -visiblity (by taking a ForAllTyBinder rathre than a TyCoVar), so that -coercionLKind/RKind build forall types that match (are equal to) the desired -ones. Otherwise we get an infinite loop in the solver via canEqCanLHSHetero. -Examples: T16946, T15079. +For now, we decide to ignore specificity. That is, we have the following: + + eqForAllVis Required Required = True + eqForAllVis (Invisible _) (Invisible _) = True + eqForAllVis _ _ = False + +One unfortunate consequence of this setup is that it can be exploited +to observe the order of inferred quantification (#22648). However, fixing this +would be a breaking change, so we choose not to (at least for now). Historical Note [Typechecker equality vs definitional equality] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -335,7 +333,7 @@ is more finer-grained than definitional equality in two places: Constraint, but typechecker treats them as distinct types. * Unlike definitional equality, which does not care about the ForAllTyFlag of a - ForAllTy, typechecker equality treats Required type variable binders as + ForAllTy, typechecker equality treated Required type variable binders as distinct from Invisible type variable binders. See Note [ForAllTy and type equality] @@ -513,9 +511,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) + go env (ForAllTy (Bndr tv1 _) t1) (ForAllTy (Bndr tv2 _) t2) + -- Ignore ForAllTyFlag. See Note [ForAllTy and type equality] + = go env (varType tv1) (varType tv2) `thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2 -- See Note [Equality on AppTys] 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) diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs index e5d7a84bb6..a42e8e4191 100644 --- a/compiler/GHC/Types/Error/Codes.hs +++ b/compiler/GHC/Types/Error/Codes.hs @@ -577,6 +577,7 @@ type family GhcDiagnosticCode c = n | n -> c where GhcDiagnosticCode "TcRnIncoherentRoles" = 18273 GhcDiagnosticCode "TcRnTyFamNameMismatch" = 88221 GhcDiagnosticCode "TcRnTypeSynonymCycle" = 97522 + GhcDiagnosticCode "TcRnIncompatibleForallVisibility" = 25115 -- PatSynInvalidRhsReason GhcDiagnosticCode "PatSynNotInvertible" = 69317 |