Commit 553c5182 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Look inside synonyms for foralls when unifying

This fixes Trac #10194
parent 8b7ceece
......@@ -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
......
......@@ -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
......
{-# LANGUAGE RankNTypes #-}
module T10194 where
type X = forall a . a
comp :: (X -> c) -> (a -> X) -> (a -> c)
comp = (.)
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 = (.)
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment