Fixes (hopefully!) T9858

The changes are:
  1. No impredicative types in `Typeable`
  2. Distinguish normal tuples, from tuples of constraints.

compiler/deSugar/DsBinds.hs

@@ -41,10 +41,11 @@ import Digraph
 import PrelNames
 import TysPrim ( mkProxyPrimTy )
 import TyCon      ( isTupleTyCon, tyConDataCons_maybe
-                  , tyConName, isPromotedTyCon, isPromotedDataCon )
+                  , tyConName, isPromotedTyCon, isPromotedDataCon, tyConKind )
 import TcEvidence
 import TcType
 import Type
+import Kind (returnsConstraintKind)
 import Coercion hiding (substCo)
 import TysWiredIn ( eqBoxDataCon, coercibleDataCon, tupleCon, mkListTy
                   , mkBoxedTupleTy, stringTy )
@@ -983,6 +984,9 @@ dsEvTypeable ev =
     hash_name_fs
       | isPromotedTyCon tc    = appendFS (mkFastString "$k") name_fs
       | isPromotedDataCon tc  = appendFS (mkFastString "$c") name_fs
+      | isTupleTyCon tc &&
+        returnsConstraintKind (tyConKind tc)
+                              = appendFS (mkFastString "$p") name_fs
       | otherwise             = name_fs
 
     hashThis = unwords $ map unpackFS [pkg_fs, modl_fs, hash_name_fs]

compiler/typecheck/TcInteract.hs

@@ -14,7 +14,7 @@ import TcCanonical
 import TcFlatten
 import VarSet
 import Type
-import Kind (isKind, isConstraintKind)
+import Kind (isKind, isConstraintKind )
 import Unify
 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
 import CoAxiom(sfInteractTop, sfInteractInert)
@@ -1846,10 +1846,14 @@ isCallStackIP _ _ _
 -- | Assumes that we've checked that this is the 'Typeable' class,
 -- and it was applied to the correct argument.
 matchTypeableClass :: Class -> Kind -> Type -> CtLoc -> TcS LookupInstResult
-matchTypeableClass clas k t loc
+matchTypeableClass clas _k t loc
+
+  -- See Note [No Typeable for qualified types]
   | isForAllTy t                               = return NoInstance
-  | isConstraintKind k                         = return NoInstance
-      -- See Note [No Typeable for qualified types]
+  -- Is the type of the form `C => t`?
+  | Just (t1,_) <- splitFunTy_maybe t,
+    isConstraintKind (typeKind t1)             = return NoInstance
+
   | Just (tc, ks) <- splitTyConApp_maybe t
   , all isKind ks                              = doTyCon tc ks
   | Just (f,kt)       <- splitAppTy_maybe t    = doTyApp f kt
@@ -1902,8 +1906,6 @@ matchTypeableClass clas k t loc
 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)
 
@@ -1914,19 +1916,9 @@ a TypeRep for them.  For qualified but not polymorphic types, like
  * 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.
+  * Perhaps we could treat `=>` as another type constructor for `Typeable`
+    purposes, and thus support things like `Eq Int => Int`, however,
+    at the current state of affairs this would be an odd exception as
+    no other class works with impredicative types.
+    For now we leave it off, until we have a better story for impredicativity.
 -}

testsuite/tests/typecheck/should_fail/T9858b.hs

@@ -0,0 +1,10 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T9858b where
+import Data.Typeable
+
+test = typeRep (Proxy :: Proxy (Eq Int => Int))
+
+
+

testsuite/tests/typecheck/should_fail/T9858b.stderr

@@ -0,0 +1,8 @@
+
+T9858b.hs:7:8: error:
+    No instance for (Typeable (Eq Int => Int))
+      (maybe you haven't applied a function to enough arguments?)
+      arising from a use of ‘typeRep’
+    In the expression: typeRep (Proxy :: Proxy (Eq Int => Int))
+    In an equation for ‘test’:
+        test = typeRep (Proxy :: Proxy (Eq Int => Int))

testsuite/tests/typecheck/should_fail/all.T

@@ -357,3 +357,4 @@ test('T9999', normal, compile_fail, [''])
 test('T10194', normal, compile_fail, [''])
 test('T8030', normal, compile_fail, [''])
 test('T9858a', normal, compile_fail, [''])
+test('T9858b', normal, compile_fail, [''])

testsuite/tests/typecheck/should_run/T9858c.hs

@@ -0,0 +1,19 @@
+{-# LANGUAGE KindSignatures #-}
+module Main(main) where
+
+import Data.Typeable
+import GHC.Exts
+
+test1 :: Bool
+test1 = typeRep (Proxy :: Proxy (() :: *)) ==
+        typeRep (Proxy :: Proxy (() :: Constraint))
+
+test2 :: Bool
+test2 = typeRepTyCon (typeRep (Proxy :: Proxy (Int,Int))) ==
+        typeRepTyCon (typeRep (Proxy :: Proxy (Eq Int, Eq Int)))
+
+main :: IO ()
+main = print (test1,test2)
+
+
+

testsuite/tests/typecheck/should_run/T9858c.stdout

@@ -0,0 +1 @@
+(False,False)

testsuite/tests/typecheck/should_run/all.T

@@ -117,3 +117,4 @@ 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, [''])
+test('T9858c', normal, compile_and_run, [''])