[commit: ghc] ghc-7.10: Fix #10285 by refusing to use NthCo on a newtype. (43e682b)
git at git.haskell.org
git at git.haskell.org
Mon May 11 10:07:26 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : ghc-7.10
Link : http://ghc.haskell.org/trac/ghc/changeset/43e682bc6a3ce86047b46e18866b87658c3ed456/ghc
>---------------------------------------------------------------
commit 43e682bc6a3ce86047b46e18866b87658c3ed456
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Thu Apr 23 15:31:37 2015 -0400
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
(cherry picked from commit a8d39a7255df187b742fecc049f0de6528b9acad)
>---------------------------------------------------------------
43e682bc6a3ce86047b46e18866b87658c3ed456
compiler/coreSyn/CoreLint.hs | 2 ++
compiler/typecheck/TcCanonical.hs | 25 ++++++++++++++---
compiler/types/Coercion.hs | 31 +++++++++++++++++++++-
testsuite/tests/typecheck/should_fail/T10285.hs | 11 ++++++++
.../tests/typecheck/should_fail/T10285.stderr | 20 ++++++++++++++
testsuite/tests/typecheck/should_fail/T10285a.hs | 11 ++++++++
testsuite/tests/typecheck/should_fail/all.T | 4 +++
7 files changed, 99 insertions(+), 5 deletions(-)
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 5ae7a59..ead384c 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1150,6 +1150,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)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 1511885..4310e35 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -710,11 +710,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]
@@ -740,6 +743,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
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 8bdb2e6..2a3da3b 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -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
@@ -491,6 +493,34 @@ necessary for soundness, but this choice removes ambiguity.
The rules here also dictate what the parameters to mkTyConAppCo.
+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}
@@ -1980,4 +2010,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.
-}
-
diff --git a/testsuite/tests/typecheck/should_fail/T10285.hs b/testsuite/tests/typecheck/should_fail/T10285.hs
new file mode 100644
index 0000000..cebdfe1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10285.hs
@@ -0,0 +1,11 @@
+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
diff --git a/testsuite/tests/typecheck/should_fail/T10285.stderr b/testsuite/tests/typecheck/should_fail/T10285.stderr
new file mode 100644
index 0000000..b56f124
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10285.stderr
@@ -0,0 +1,20 @@
+
+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
diff --git a/testsuite/tests/typecheck/should_fail/T10285a.hs b/testsuite/tests/typecheck/should_fail/T10285a.hs
new file mode 100644
index 0000000..53a468b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10285a.hs
@@ -0,0 +1,11 @@
+{-# 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
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 8ae6410..c4a9fc8 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -355,3 +355,7 @@ test('T4921', normal, compile_fail, [''])
test('T9605', normal, compile_fail, [''])
test('T9999', normal, compile_fail, [''])
test('T10194', normal, compile_fail, [''])
+
+test('T10285',
+ extra_clean(['T10285a.hi', 'T10285a.o']),
+ multimod_compile_fail, ['T10285', '-v0'])
More information about the ghc-commits
mailing list