Commit a8d39a72 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #10285 by refusing to use NthCo on a newtype.

During this commit, I tested to make sure that CoreLint actually
catches the Core error if the typechecker doesn't.

Test case: typecheck/should_fail/T10285
parent 6ab5da99
......@@ -9,14 +9,14 @@ A ``lint'' pass to check for Core correctness
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fprof-auto #-}
module CoreLint (
lintCoreBindings, lintUnfolding,
module CoreLint (
lintCoreBindings, lintUnfolding,
lintPassResult, lintInteractiveExpr, lintExpr,
lintAnnots,
-- ** Debug output
CoreLint.showPass, showPassIO, endPass, endPassIO,
dumpPassResult,
CoreLint.showPass, showPassIO, endPass, endPassIO,
dumpPassResult,
CoreLint.dumpIfSet,
) where
......@@ -1255,6 +1255,8 @@ lintCoercion the_co@(NthCo n co)
; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
(Just (tc_s, tys_s), Just (tc_t, tys_t))
| tc_s == tc_t
, isDistinctTyCon tc_s || r /= Representational
-- see Note [NthCo and newtypes] in Coercion
, tys_s `equalLength` tys_t
, n < length tys_s
-> return (ks, ts, tt, tr)
......@@ -1389,7 +1391,7 @@ lintCoercion this@(AxiomRuleCo co ts cs)
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism]
data LintEnv
data LintEnv
= LE { le_flags :: LintFlags -- Linting the result of this pass
, le_loc :: [LintLocInfo] -- Locations
, le_subst :: TvSubst -- Current type substitution; we also use this
......@@ -1512,7 +1514,7 @@ addMsg env msgs msg
addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc extra_loc m
= LintM $ \ env errs ->
= LintM $ \ env errs ->
unLintM m (env { le_loc = extra_loc : le_loc env }) errs
inCasePat :: LintM Bool -- A slight hack; see the unique call site
......@@ -1523,18 +1525,18 @@ inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
addInScopeVars :: [Var] -> LintM a -> LintM a
addInScopeVars vars m
= LintM $ \ env errs ->
unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
= LintM $ \ env errs ->
unLintM m (env { le_subst = extendTvInScopeList (le_subst env) vars })
errs
addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar var m
= LintM $ \ env errs ->
= LintM $ \ env errs ->
unLintM m (env { le_subst = extendTvInScope (le_subst env) var }) errs
extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
= LintM $ \ env errs ->
= LintM $ \ env errs ->
unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
updateTvSubst :: TvSubst -> LintM a -> LintM a
......
{-# LANGUAGE CPP #-}
module TcCanonical(
module TcCanonical(
canonicalize,
unifyDerived,
......@@ -684,11 +684,14 @@ canDecomposableTyConApp :: CtEvidence -> EqRel
-- See Note [Decomposing TyConApps]
canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
| tc1 == tc2
, length tys1 == length tys2 -- Success: decompose!
= do { traceTcS "canDecomposableTyConApp"
, length tys1 == length tys2
= if eq_rel == NomEq || ctEvFlavour ev /= Given || isDistinctTyCon tc1
-- See Note [Decomposing newtypes]
then do { traceTcS "canDecomposableTyConApp"
(ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
; stopWith ev "Decomposed TyConApp" }
; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
; stopWith ev "Decomposed TyConApp" }
else canEqFailure ev eq_rel ty1 ty2
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
......@@ -714,6 +717,20 @@ Here is the case:
Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
know `a`. This is *not* a hard failure, because we might soon learn
that `a` is, in fact, Char, and then the equality succeeds.
Note [Decomposing newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
As explained in Note [NthCo and newtypes] in Coercion, we can't use
NthCo on representational coercions over newtypes. So we avoid doing
so.
But is it sensible to decompose *Wanted* constraints over newtypes?
Yes. By the time we reach canDecomposableTyConApp, we know that any
newtypes that can be unwrapped have been. So, without importing more
constructors, say, we know there is no way forward other than decomposition.
So we take the one route we have available. This *does* mean that
importing a newtype's constructor might make code that previously
compiled fail to do so. (If that newtype is perversely recursive, say.)
-}
canDecomposableTyConAppOK :: CtEvidence -> EqRel
......@@ -1314,7 +1331,7 @@ rewriteEvidence old_ev new_pred co
= return (ContinueWith (old_ev { ctev_pred = new_pred }))
rewriteEvidence ev@(CtGiven { ctev_evar = old_evar , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm)
; return (ContinueWith new_ev) }
where
-- mkEvCast optimises ReflCo
......
......@@ -190,6 +190,8 @@ data Coercion
| NthCo Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
-- :: _ -> e -> ?? (inverse of TyConAppCo, see Note [TyConAppCo roles])
-- See Note [NthCo and newtypes]
| LRCo LeftOrRight Coercion -- Decomposes (t_left t_right)
-- :: _ -> N -> N
| InstCo Coercion Type
......@@ -496,6 +498,34 @@ TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
The rules here dictate the roles of the parameters to mkTyConAppCo
(should be checked by Lint).
Note [NthCo and newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
newtype N a = MkN Int
type role N representational
This yields axiom
NTCo:N :: forall a. N a ~R Int
We can then build
co :: forall a b. N a ~R N b
co = NTCo:N a ; sym (NTCo:N b)
for any `a` and `b`. Because of the role annotation on N, if we use
NthCo, we'll get out a representational coercion. That is:
NthCo 0 co :: forall a b. a ~R b
Yikes! Clearly, this is terrible. The solution is simple: forbid
NthCo to be used on newtypes if the internal coercion is representational.
This is not just some corner case discovered by a segfault somewhere;
it was discovered in the proof of soundness of roles and described
in the "Safe Coercions" paper (ICFP '14).
************************************************************************
* *
\subsection{Coercion variables}
......@@ -1988,4 +2018,3 @@ Kind coercions are only of the form: Refl kind. They are only used to
instantiate kind polymorphic type constructors in TyConAppCo. Remember
that kind instantiation only happens with TyConApp, not AppTy.
-}
module T10285 where
import T10285a
import Data.Type.Coercion
import Data.Coerce
oops :: Coercion (N a) (N b) -> a -> b
oops Coercion = coerce
unsafeCoerce :: a -> b
unsafeCoerce = oops coercion
T10285.hs:8:17: error:
Could not deduce: a ~ b
from the context: Coercible (N a) (N b)
bound by a pattern with constructor:
Coercion :: forall (k :: BOX) (a :: k) (b :: k).
Coercible a b =>
Coercion a b,
in an equation for ‘oops’
at T10285.hs:8:6-13
‘a’ is a rigid type variable bound by
the type signature for: oops :: Coercion (N a) (N b) -> a -> b
at T10285.hs:7:9
‘b’ is a rigid type variable bound by
the type signature for: oops :: Coercion (N a) (N b) -> a -> b
at T10285.hs:7:9
Relevant bindings include
oops :: Coercion (N a) (N b) -> a -> b (bound at T10285.hs:8:1)
In the expression: coerce
In an equation for ‘oops’: oops Coercion = coerce
{-# LANGUAGE RoleAnnotations #-}
module T10285a (N, coercion) where
import Data.Type.Coercion
newtype N a = MkN Int
type role N representational
coercion :: Coercion (N a) (N b)
coercion = Coercion
......@@ -359,3 +359,7 @@ test('T8030', normal, compile_fail, [''])
test('T9858a', normal, compile_fail, [''])
test('T9858b', normal, compile_fail, [''])
test('T9858e', normal, compile_fail, [''])
test('T10285',
extra_clean(['T10285a.hi', 'T10285a.o']),
multimod_compile_fail, ['T10285', '-v0'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment