Look inside synonyms for foralls when unifying

This fixes Trac #10194

5 files changed, 26 insertions, 4 deletions

diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 42c9af3aa7..ca1ecaa55c 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -859,7 +859,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'
@@ -1234,7 +1234,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
@@ -1268,7 +1268,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 f732515808..754d3108e0 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1026,10 +1026,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 0000000000..2174a59240
--- /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 0000000000..53ee74b93c
--- /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 7efbb70ce1..ea53e39d69 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, [''])