[commit: ghc] master: Fix #10285 by refusing to use NthCo on a newtype. (a8d39a7)

git at git.haskell.org git at git.haskell.org
Fri Apr 24 21:02:11 UTC 2015


Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/a8d39a7255df187b742fecc049f0de6528b9acad/ghc

>---------------------------------------------------------------

commit a8d39a7255df187b742fecc049f0de6528b9acad
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


>---------------------------------------------------------------

a8d39a7255df187b742fecc049f0de6528b9acad
 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 256a682..ec0bb5e 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -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)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 80768a6..e9e35a4 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -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
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index e6e21b1..797f785 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
@@ -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.
 -}
-
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 abddd3e..110f29f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -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'])



More information about the ghc-commits mailing list