diff options
-rw-r--r-- | compiler/GHC/Core/Type.hs | 71 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T19742.hs | 20 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 |
3 files changed, 72 insertions, 20 deletions
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 5ed621d404..aed365656a 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -1528,33 +1528,64 @@ splitCastTy_maybe ty -- | Make a 'CastTy'. The Coercion must be nominal. Checks the -- Coercion for reflexivity, dropping it if it's reflexive. --- See Note [Respecting definitional equality] in "GHC.Core.TyCo.Rep" +-- See @Note [Respecting definitional equality]@ in "GHC.Core.TyCo.Rep" mkCastTy :: Type -> Coercion -> Type -mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note +mkCastTy orig_ty co | isReflexiveCo co = orig_ty -- (EQ2) from the Note -- NB: Do the slow check here. This is important to keep the splitXXX -- functions working properly. Otherwise, we may end up with something -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz) -- fails under splitFunTy_maybe. This happened with the cheaper check -- in test dependent/should_compile/dynamic-paper. +mkCastTy orig_ty co = mk_cast_ty orig_ty co -mkCastTy (CastTy ty co1) co2 - -- (EQ3) from the Note - = mkCastTy ty (co1 `mkTransCo` co2) - -- call mkCastTy again for the reflexivity check - -mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co - -- (EQ4) from the Note - -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep. - | isTyVar tv - , let fvs = tyCoVarsOfCo co - = -- have to make sure that pushing the co in doesn't capture the bound var! - if tv `elemVarSet` fvs - then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs) - (subst, tv') = substVarBndr empty_subst tv - in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mkCastTy` co) - else ForAllTy (Bndr tv vis) (inner_ty `mkCastTy` co) - -mkCastTy ty co = CastTy ty co +-- | Like 'mkCastTy', but avoids checking the coercion for reflexivity, +-- as that can be expensive. +mk_cast_ty :: Type -> Coercion -> Type +mk_cast_ty orig_ty co = go orig_ty + where + go :: Type -> Type + -- See Note [Using coreView in mk_cast_ty] + go ty | Just ty' <- coreView ty = go ty' + + go (CastTy ty co1) + -- (EQ3) from the Note + = mkCastTy ty (co1 `mkTransCo` co) + -- call mkCastTy again for the reflexivity check + + go (ForAllTy (Bndr tv vis) inner_ty) + -- (EQ4) from the Note + -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep. + | isTyVar tv + , let fvs = tyCoVarsOfCo co + = -- have to make sure that pushing the co in doesn't capture the bound var! + if tv `elemVarSet` fvs + then let empty_subst = mkEmptyTCvSubst (mkInScopeSet fvs) + (subst, tv') = substVarBndr empty_subst tv + in ForAllTy (Bndr tv' vis) (substTy subst inner_ty `mk_cast_ty` co) + else ForAllTy (Bndr tv vis) (inner_ty `mk_cast_ty` co) + + go _ = CastTy orig_ty co -- NB: orig_ty: preserve synonyms if possible + +{- +Note [Using coreView in mk_cast_ty] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Invariants (EQ3) and (EQ4) of Note [Respecting definitional equality] in +GHC.Core.TyCo.Rep must apply regardless of type synonyms. For instance, +consider this example (#19742): + + type EqSameNat = () |> co + useNatEq :: EqSameNat |> sym co + +(Those casts aren't visible in the user-source code, of course; see #19742 for +what the user might write.) + +The type `EqSameNat |> sym co` looks as if it satisfies (EQ3), as it has no +nested casts, but if we expand EqSameNat, we see that it doesn't. +And then Bad Things happen. + +The solution is easy: just use `coreView` when establishing (EQ3) and (EQ4) in +`mk_cast_ty`. +-} tyConBindersTyCoBinders :: [TyConBinder] -> [TyCoBinder] -- Return the tyConBinders in TyCoBinder form diff --git a/testsuite/tests/typecheck/should_compile/T19742.hs b/testsuite/tests/typecheck/should_compile/T19742.hs new file mode 100644 index 0000000000..c6489976bd --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T19742.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} +module T19742 where + +import Data.Kind + +type Id :: Type -> Type +type family Id x where + Id x = x + +type EqSameNat :: Id Type +type EqSameNat = () + +useNatEq :: EqSameNat +useNatEq = () + +decCongS :: () +decCongS = case useNatEq of () -> () diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index b02d64adcc..9b3753848f 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -783,3 +783,4 @@ test('T18467', normal, compile, ['']) test('T19315', normal, compile, ['']) test('T19535', normal, compile, ['']) +test('T19742', normal, compile, ['']) |