[commit: ghc] master: Do not allow Typeable on constraints (Trac #9858) (7b042d5)
git at git.haskell.org
git at git.haskell.org
Tue Apr 14 14:40:24 UTC 2015
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/7b042d5adabdb0fc06286db1a7f9cbf1e9fd1fbf/ghc
>---------------------------------------------------------------
commit 7b042d5adabdb0fc06286db1a7f9cbf1e9fd1fbf
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Tue Apr 14 15:39:01 2015 +0100
Do not allow Typeable on constraints (Trac #9858)
The astonishingly-ingenious trio of
Shachaf Ben-Kiki, Ørjan Johansen and Nathan van Doorn
managed to persuade GHC 7.10.1 to cough up unsafeCoerce.
That is very bad. This patch fixes it by no allowing Typable
on Constraint-kinded things. And that seems right, since
it is, in effect, a form of impredicative polymorphism,
which Typeable definitely doesn't support.
We may want to creep back in the direction of allowing
Typeable on constraints one day, but this is a good
fix for now, and closes a terrible hole.
>---------------------------------------------------------------
7b042d5adabdb0fc06286db1a7f9cbf1e9fd1fbf
compiler/typecheck/TcInteract.hs | 39 ++++++++++++++++++++--
compiler/types/TypeRep.hs | 14 ++++++--
testsuite/tests/typecheck/should_fail/T9858a.hs | 35 +++++++++++++++++++
.../tests/typecheck/should_fail/T9858a.stderr | 12 +++++++
testsuite/tests/typecheck/should_fail/all.T | 1 +
testsuite/tests/typecheck/should_run/T9858b.hs | 8 +++++
.../tests/typecheck/should_run/T9858b.stdout | 0
testsuite/tests/typecheck/should_run/all.T | 1 +
8 files changed, 106 insertions(+), 4 deletions(-)
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 8494153..271f973 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -14,7 +14,7 @@ import TcCanonical
import TcFlatten
import VarSet
import Type
-import Kind (isKind)
+import Kind (isKind, isConstraintKind)
import Unify
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
import CoAxiom(sfInteractTop, sfInteractInert)
@@ -1847,7 +1847,9 @@ isCallStackIP _ _ _
-- and it was applied to the correct argument.
matchTypeableClass :: Class -> Kind -> Type -> CtLoc -> TcS LookupInstResult
matchTypeableClass clas k t loc
- | isForAllTy k = return NoInstance
+ | isForAllTy t = return NoInstance
+ | isConstraintKind k = return NoInstance
+ -- See Note [No Typeable for qualified types]
| Just (tc, ks) <- splitTyConApp_maybe t
, all isKind ks = doTyCon tc ks
| Just (f,kt) <- splitAppTy_maybe t = doTyApp f kt
@@ -1895,3 +1897,36 @@ matchTypeableClass clas k t loc
mkSimpEv ev = return (GenInst [] (EvTypeable ev))
+{- Note [No Typeable for polytype or for constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We do not support impredicative typeable, such as
+ Typeable (forall a. a->a)
+ Typeable (Eq a => a -> a)
+ Typeable (Eq a)
+ Typeable (() :: Constraint)
+ Typeable (() => Int)
+ Typeable (((),()) => Int)
+
+See Trac #9858. For forall's the case is clear: we simply don't have
+a TypeRep for them. For qualified but not polymorphic types, like
+(Eq a => a -> a), things are murkier. But:
+
+ * We don't need a TypeRep for these things. TypeReps are for
+ monotypes only.
+
+ * The types (Eq a, Show a) => ...blah...
+ and Eq a => Show a => ...blah...
+ are represented the same way, as a curried function;
+ that is, the tuple before the '=>' is just syntactic
+ sugar. But since we can abstract over tuples of constraints,
+ we really do have tuples of constraints as well.
+
+ This dichotomy is not well worked out, and Trac #9858 comment:76
+ shows that Typeable treated it one way, while newtype instance
+ matching treated it another. Or maybe it was the fact that
+ '*' and Constraint are distinct to the type checker, but are
+ the same afterwards. Anyway, the result was a function of
+ type (forall ab. a -> b), which is pretty dire.
+
+So the simple solution is not to attempt Typable for constraints.
+-}
diff --git a/compiler/types/TypeRep.hs b/compiler/types/TypeRep.hs
index 3e46de3..8ed07c1 100644
--- a/compiler/types/TypeRep.hs
+++ b/compiler/types/TypeRep.hs
@@ -730,8 +730,7 @@ pprTcApp _ pp tc [ty]
pprTcApp p pp tc tys
| isTupleTyCon tc && tyConArity tc == length tys
- = pprPromotionQuote tc <>
- tupleParens (tupleTyConSort tc) (sep (punctuate comma (map (pp TopPrec) tys)))
+ = pprTupleApp p pp tc tys
| Just dc <- isPromotedDataCon_maybe tc
, let dc_tc = dataConTyCon dc
@@ -746,6 +745,17 @@ pprTcApp p pp tc tys
| otherwise
= sdocWithDynFlags (pprTcApp_help p pp tc tys)
+pprTupleApp :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
+-- Print a saturated tuple
+pprTupleApp p pp tc tys
+ | null tys
+ , ConstraintTuple <- tupleTyConSort tc
+ = maybeParen p TopPrec $
+ ppr tc <+> dcolon <+> ppr (tyConKind tc)
+ | otherwise
+ = pprPromotionQuote tc <>
+ tupleParens (tupleTyConSort tc) (sep (punctuate comma (map (pp TopPrec) tys)))
+
pprTcApp_help :: TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> DynFlags -> SDoc
-- This one has accss to the DynFlags
pprTcApp_help p pp tc tys dflags
diff --git a/testsuite/tests/typecheck/should_fail/T9858a.hs b/testsuite/tests/typecheck/should_fail/T9858a.hs
new file mode 100644
index 0000000..fda55c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T9858a.hs
@@ -0,0 +1,35 @@
+-- From comment:76 in Trac #9858
+-- This exploit still works in GHC 7.10.1.
+-- By Shachaf Ben-Kiki, Ørjan Johansen and Nathan van Doorn
+
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module T9858a where
+
+import Data.Typeable
+
+type E = (:~:)
+type PX = Proxy (((),()) => ())
+type PY = Proxy (() -> () -> ())
+
+data family F p a b
+
+newtype instance F a b PX = ID (a -> a)
+newtype instance F a b PY = UC (a -> b)
+
+{-# NOINLINE ecast #-}
+ecast :: E p q -> f p -> f q
+ecast Refl = id
+
+supercast :: F a b PX -> F a b PY
+supercast = case cast e of
+ Just e' -> ecast e'
+ where
+ e = Refl
+ e :: E PX PX
+
+uc :: a -> b
+uc = case supercast (ID id) of UC f -> f
diff --git a/testsuite/tests/typecheck/should_fail/T9858a.stderr b/testsuite/tests/typecheck/should_fail/T9858a.stderr
new file mode 100644
index 0000000..72b72e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T9858a.stderr
@@ -0,0 +1,12 @@
+
+T9858a.hs:28:18: error:
+ No instance for (Typeable (() :: Constraint))
+ arising from a use of ‘cast’
+ In the expression: cast e
+ In the expression: case cast e of { Just e' -> ecast e' }
+ In an equation for ‘supercast’:
+ supercast
+ = case cast e of { Just e' -> ecast e' }
+ where
+ e = Refl
+ e :: E PX PX
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 5d31bcd..ac91670 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -356,3 +356,4 @@ test('T9605', normal, compile_fail, [''])
test('T9999', normal, compile_fail, [''])
test('T10194', normal, compile_fail, [''])
test('T8030', normal, compile_fail, [''])
+test('T9858a', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_run/T9858b.hs b/testsuite/tests/typecheck/should_run/T9858b.hs
new file mode 100644
index 0000000..3c680c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T9858b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE DataKinds #-}
+module Main where
+
+import Data.Typeable
+
+data A = A
+
+main = print $ typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy 'A)
diff --git a/libraries/base/tests/dynamic003.stdout b/testsuite/tests/typecheck/should_run/T9858b.stdout
similarity index 100%
copy from libraries/base/tests/dynamic003.stdout
copy to testsuite/tests/typecheck/should_run/T9858b.stdout
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index f0a5eb6..4868db3 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -116,3 +116,4 @@ test('T8739', normal, compile_and_run, [''])
test('T9497a-run', [exit_code(1)], compile_and_run, ['-fdefer-typed-holes'])
test('T9497b-run', [exit_code(1)], compile_and_run, ['-fdefer-typed-holes -fno-warn-typed-holes'])
test('T9497c-run', [exit_code(1)], compile_and_run, ['-fdefer-type-errors -fno-warn-typed-holes'])
+test('T9858b', normal, compile_and_run, [''])
More information about the ghc-commits
mailing list