[commit: ghc] ghc-7.10: Look inside synonyms for foralls when unifying (681d82c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-7.10
Link       : http://ghc.haskell.org/trac/ghc/changeset/681d82c0d44f06f0b958b75778c30b0910df982b/ghc

>---------------------------------------------------------------

commit 681d82c0d44f06f0b958b75778c30b0910df982b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Apr 7 14:45:04 2015 +0100

    Look inside synonyms for foralls when unifying
    
    This fixes Trac #10194
    
    (cherry picked from commit 553c5182156c5e4c15e3bd1c17c6d83a95a6c408)


>---------------------------------------------------------------

681d82c0d44f06f0b958b75778c30b0910df982b
 compiler/typecheck/TcType.hs                        | 10 +++++++---
 compiler/typecheck/TcUnify.hs                       |  5 ++++-
 testsuite/tests/typecheck/should_fail/T10194.hs     |  7 +++++++
 testsuite/tests/typecheck/should_fail/T10194.stderr |  7 +++++++
 testsuite/tests/typecheck/should_fail/all.T         |  1 +
 5 files changed, 26 insertions(+), 4 deletions(-)

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 2d567ce..b7dc58e 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -853,7 +853,7 @@ mkTcEqPredRole Nominal          = mkTcEqPred
 mkTcEqPredRole Representational = mkTcReprEqPred
 mkTcEqPredRole Phantom          = panic "mkTcEqPredRole Phantom"
 
--- @isTauTy@ tests for nested for-alls.  It should not be called on a boxy type.
+-- @isTauTy@ tests for nested for-alls.
 
 isTauTy :: Type -> Bool
 isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
@@ -1228,7 +1228,7 @@ occurCheckExpand dflags tv ty
     -- True => fine
     fast_check (LitTy {})        = True
     fast_check (TyVarTy tv')     = tv /= tv'
-    fast_check (TyConApp _ tys)  = all fast_check tys
+    fast_check (TyConApp tc tys) = all fast_check tys && (isTauTyCon tc || impredicative)
     fast_check (FunTy arg res)   = fast_check arg && fast_check res
     fast_check (AppTy fun arg)   = fast_check fun && fast_check arg
     fast_check (ForAllTy tv' ty) = impredicative
@@ -1262,7 +1262,11 @@ occurCheckExpand dflags tv ty
     -- it and try again.
     go ty@(TyConApp tc tys)
       = case do { tys <- mapM go tys; return (mkTyConApp tc tys) } of
-          OC_OK ty -> return ty  -- First try to eliminate the tyvar from the args
+          OC_OK ty
+              | impredicative || isTauTyCon tc
+              -> return ty  -- First try to eliminate the tyvar from the args
+              | otherwise
+              -> OC_Forall  -- A type synonym with a forall on the RHS
           bad | Just ty' <- tcView ty -> go ty'
               | otherwise             -> bad
                       -- Failing that, try to expand a synonym
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index b4a6ada..ef21d87 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1012,10 +1012,13 @@ checkTauTvUpdate dflags tv ty
     defer_me :: TcType -> Bool
     -- Checks for (a) occurrence of tv
     --            (b) type family applications
+    --            (c) foralls
     -- See Note [Conservative unification check]
     defer_me (LitTy {})        = False
     defer_me (TyVarTy tv')     = tv == tv'
-    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
+    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc
+                                 || any defer_me tys
+                                 || not (impredicative || isTauTyCon tc)
     defer_me (FunTy arg res)   = defer_me arg || defer_me res
     defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
     defer_me (ForAllTy _ ty)   = not impredicative || defer_me ty
diff --git a/testsuite/tests/typecheck/should_fail/T10194.hs b/testsuite/tests/typecheck/should_fail/T10194.hs
new file mode 100644
index 0000000..2174a59
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10194.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+module T10194 where
+
+type X = forall a . a
+
+comp :: (X -> c) -> (a -> X) -> (a -> c)
+comp = (.)
diff --git a/testsuite/tests/typecheck/should_fail/T10194.stderr b/testsuite/tests/typecheck/should_fail/T10194.stderr
new file mode 100644
index 0000000..53ee74b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T10194.stderr
@@ -0,0 +1,7 @@
+
+T10194.hs:7:8:
+    Cannot instantiate unification variable ‘b0’
+    with a type involving foralls: X
+      Perhaps you want ImpredicativeTypes
+    In the expression: (.)
+    In an equation for ‘comp’: comp = (.)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index f5d4d0e..8ae6410 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -354,3 +354,4 @@ test('T8044', normal, compile_fail, [''])
 test('T4921', normal, compile_fail, [''])
 test('T9605', normal, compile_fail, [''])
 test('T9999', normal, compile_fail, [''])
+test('T10194', normal, compile_fail, [''])