Look inside synonyms for foralls when unifying
authorSimon Peyton Jones <simonpj@microsoft.com>
Tue, 7 Apr 2015 13:45:04 +0000 (14:45 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Tue, 7 Apr 2015 14:10:48 +0000 (15:10 +0100)
This fixes Trac #10194

compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
testsuite/tests/typecheck/should_fail/T10194.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T10194.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/all.T

index 42c9af3..ca1ecaa 100644 (file)
@@ -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
index f732515..754d310 100644 (file)
@@ -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 (file)
index 0000000..2174a59
--- /dev/null
@@ -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 (file)
index 0000000..53ee74b
--- /dev/null
@@ -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 = (.)
index 7efbb70..ea53e39 100644 (file)
@@ -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, [''])