From 60b03adea8cc55ff65fbf6458487c3baf12bb0a1 Mon Sep 17 00:00:00 2001 From: Krzysztof Gogolewski Date: Thu, 7 Mar 2019 17:19:45 +0100 Subject: [PATCH 1/2] Change the warning in substTy back to an assertion We'd like to enforce the substitution invariant (Trac #11371). In a492af06d326453 the assertion was downgraded to a warning; I'm restoring the assertion and making the calls that don't maintain the invariant as unchecked. --- compiler/coreSyn/CoreArity.hs | 2 +- compiler/typecheck/TcGenGenerics.hs | 2 +- compiler/typecheck/TcSigs.hs | 2 +- compiler/types/TyCoRep.hs | 5 ++--- 4 files changed, 5 insertions(+), 6 deletions(-) diff --git a/compiler/coreSyn/CoreArity.hs b/compiler/coreSyn/CoreArity.hs index 37454ebee08..afd6759571c 100644 --- a/compiler/coreSyn/CoreArity.hs +++ b/compiler/coreSyn/CoreArity.hs @@ -1153,7 +1153,7 @@ freshEtaId :: Int -> TCvSubst -> Type -> (TCvSubst, Id) freshEtaId n subst ty = (subst', eta_id') where - ty' = Type.substTy subst ty + ty' = Type.substTyUnchecked subst ty eta_id' = uniqAway (getTCvInScope subst) $ mkSysLocalOrCoVar (fsLit "eta") (mkBuiltinUnique n) ty' subst' = extendTCvInScope subst eta_id' diff --git a/compiler/typecheck/TcGenGenerics.hs b/compiler/typecheck/TcGenGenerics.hs index abc7d59a552..123cfd35352 100644 --- a/compiler/typecheck/TcGenGenerics.hs +++ b/compiler/typecheck/TcGenGenerics.hs @@ -431,7 +431,7 @@ tc_mkRepFamInsts gk tycon inst_tys = env = zipTyEnv env_tyvars env_inst_args in_scope = mkInScopeSet (tyCoVarsOfTypes inst_tys) subst = mkTvSubst in_scope env - repTy' = substTy subst repTy + repTy' = substTyUnchecked subst repTy tcv' = tyCoVarsOfTypeList inst_ty (tv', cv') = partition isTyVar tcv' tvs' = scopedSort tv' diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index 9146b10fe29..7b00165c523 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -505,7 +505,7 @@ tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty , sig_inst_wcs = wcs , sig_inst_wcx = wcx , sig_inst_theta = substTys subst theta - , sig_inst_tau = substTy subst tau } + , sig_inst_tau = substTyUnchecked subst tau } ; traceTc "End partial sig }" (ppr inst_sig) ; return inst_sig } diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 9ccfaae31d6..27fde886132 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -3196,8 +3196,7 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) = -- Note [The substitution invariant]. checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a --- TODO (RAE): Change back to ASSERT - = WARN( not (isValidTCvSubst subst), + = ASSERT2( isValidTCvSubst subst, text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ text "tenvFVs" <+> ppr (tyCoVarsOfTypesSet tenv) $$ @@ -3205,7 +3204,7 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a text "cenvFVs" <+> ppr (tyCoVarsOfCosSet cenv) $$ text "tys" <+> ppr tys $$ text "cos" <+> ppr cos ) - WARN( not tysCosFVsInScope, + ASSERT2( tysCosFVsInScope, text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ text "cenv" <+> ppr cenv $$ -- GitLab From 2f453414c5b1b27b6a84a3b5c7cd1bb5449f1f5d Mon Sep 17 00:00:00 2001 From: Krzysztof Gogolewski Date: Thu, 7 Mar 2019 19:08:59 +0100 Subject: [PATCH 2/2] Add a test for Trac #13951 It no longer gives a warning. --- .../tests/typecheck/should_compile/T13951.hs | 19 +++++++++++++++++++ .../tests/typecheck/should_compile/all.T | 1 + 2 files changed, 20 insertions(+) create mode 100644 testsuite/tests/typecheck/should_compile/T13951.hs diff --git a/testsuite/tests/typecheck/should_compile/T13951.hs b/testsuite/tests/typecheck/should_compile/T13951.hs new file mode 100644 index 00000000000..8cbeb8c11ac --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T13951.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE PolyKinds, GADTs, Rank2Types, ScopedTypeVariables, Trustworthy #-} +module Control.Monad.Skeleton.Internal where + +data Cat k a b where + Empty :: Cat k a a + Leaf :: k a b -> Cat k a b + Tree :: Cat k a b -> Cat k b c -> Cat k a c + +viewL :: forall k a b r. Cat k a b + -> ((a ~ b) => r) + -> (forall x. k a x -> Cat k x b -> r) + -> r +viewL Empty e _ = e +viewL (Leaf k) _ r = k `r` Empty +viewL (Tree a b) e r = go a b where + go :: Cat k a x -> Cat k x b -> r + go Empty t = viewL t e r + go (Leaf k) t = r k t + go (Tree c d) t = go c (Tree d t) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index d312f5074dc..b94f0210585 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -669,3 +669,4 @@ test('T16188', normal, compile, ['']) test('T16204a', normal, compile, ['']) test('T16204b', normal, compile, ['']) test('T16225', normal, compile, ['']) +test('T13951', normal, compile, ['']) -- GitLab