diff options
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 39 | ||||
-rw-r--r-- | compiler/types/TypeRep.hs | 14 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T9858a.hs | 35 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T9858a.stderr | 12 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_run/T9858b.hs | 8 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_run/T9858b.stdout | 1 | ||||
-rwxr-xr-x | testsuite/tests/typecheck/should_run/all.T | 1 |
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, ['']) |