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.

8 files changed, 107 insertions, 4 deletions

diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 84941531f7..271f973013 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 3e46de342a..8ed07c12d2 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 0000000000..fda55c20db
--- /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 0000000000..72b72e9ad3
--- /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 5d31bcdc6c..ac91670b84 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 0000000000..3c680c210d
--- /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/testsuite/tests/typecheck/should_run/T9858b.stdout b/testsuite/tests/typecheck/should_run/T9858b.stdout
new file mode 100644
index 0000000000..bc59c12aa1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T9858b.stdout
@@ -0,0 +1 @@
+False
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index f0a5eb617c..4868db3b1e 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, [''])