Commit 7b042d5a authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 6dd2765a
......@@ -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.
-}
......@@ -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
......
-- 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
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
......@@ -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, [''])
{-# LANGUAGE DataKinds #-}
module Main where
import Data.Typeable
data A = A
main = print $ typeRep (Proxy :: Proxy A) == typeRep (Proxy :: Proxy 'A)
......@@ -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, [''])
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