Commit 3e1b8824 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Prevent eager unification with type families.

See Note [Prevent unification with type families]
in TcUnify for the details.
parent f8ab5754
......@@ -1432,6 +1432,10 @@ We have
occurCheckExpand b (F (G b)) = F Char
even though we could also expand F to get rid of b.
The two variants of the function are to support TcUnify.checkTauTvUpdate,
which wants to prevent unification with type families. For more on this
point, see Note [Prevent unification with type families] in TcUnify.
See also Note [occurCheckExpand] in TcCanonical
-}
......@@ -1449,10 +1453,10 @@ instance Applicative OccCheckResult where
(<*>) = ap
instance Monad OccCheckResult where
OC_OK x >>= k = k x
OC_Forall >>= _ = OC_Forall
OC_NonTyVar >>= _ = OC_NonTyVar
OC_Occurs >>= _ = OC_Occurs
OC_OK x >>= k = k x
OC_Forall >>= _ = OC_Forall
OC_NonTyVar >>= _ = OC_NonTyVar
OC_Occurs >>= _ = OC_Occurs
occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
-- See Note [Occurs check expansion]
......@@ -1466,7 +1470,6 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
-- version of the type, which is guaranteed to be syntactically free
-- of the given type variable. If the type is already syntactically
-- free of the variable, then the same type is returned.
occurCheckExpand dflags tv ty
| MetaTv { mtv_info = SigTv } <- details
= go_sig_tv ty
......@@ -1488,7 +1491,8 @@ occurCheckExpand dflags tv ty
-- True => fine
fast_check (LitTy {}) = True
fast_check (TyVarTy tv') = tv /= tv' && fast_check (tyVarKind tv')
fast_check (TyConApp tc tys) = all fast_check tys && (isTauTyCon tc || impredicative)
fast_check (TyConApp tc tys) = all fast_check tys
&& (isTauTyCon tc || impredicative)
fast_check (ForAllTy (Anon a) r) = fast_check a && fast_check r
fast_check (AppTy fun arg) = fast_check fun && fast_check arg
fast_check (ForAllTy (Named tv' _) ty)
......
......@@ -49,6 +49,7 @@ import Inst
import TyCon
import TysWiredIn
import Var
import VarSet
import VarEnv
import ErrUtils
import DynFlags
......@@ -1440,16 +1441,91 @@ checkTauTvUpdate dflags origin t_or_k tv ty
| otherwise
= do { ty <- zonkTcType ty
; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
; return $ case occurCheckExpand dflags tv ty of
OC_OK ty2 -> Just (ty2, co_k)
_ -> Nothing }
; if | defer_me ty -> -- Quick test
-- Failed quick test so try harder
case occurCheckExpand dflags tv ty of
OC_OK ty2 | defer_me ty2 -> return Nothing
| otherwise -> return (Just (ty2, co_k))
_ -> return Nothing
| otherwise -> return (Just (ty, co_k)) }
where
kind_origin = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
details = tcTyVarDetails tv
info = mtv_info details
impredicative = canUnifyWithPolyType dflags details
defer_me :: TcType -> Bool
-- Checks for (a) occurrence of tv
-- (b) type family applications
-- (c) foralls
-- See Note [Prevent unification with type families]
-- See Note [Refactoring hazard: checkTauTvUpdate]
defer_me (LitTy {}) = False
defer_me (TyVarTy tv') = tv == tv' || defer_me (tyVarKind tv')
defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
|| not (impredicative || isTauTyCon tc)
defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t
|| (isNamedBinder bndr && not impredicative)
defer_me (AppTy fun arg) = defer_me fun || defer_me arg
defer_me (CastTy ty co) = defer_me ty || defer_me_co co
defer_me (CoercionTy co) = defer_me_co co
-- We don't really care if there are type families in a coercion,
-- but we still can't have an occurs-check failure
defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
{-
Note [Prevent unification with type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prevent unification with type families because of an uneasy compromise.
It's perfectly sound to unify with type families, and it even improves the
error messages in the testsuite. It also modestly improves performance, at
least in some cases. But it's disastrous for test case perf/compiler/T3064.
Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
What do we do? Do we reduce F? Or do we use the given? Hard to know what's
best. GHC reduces. This is a disaster for T3064, where the type's size
spirals out of control during reduction. (We're not helped by the fact that
the flattener re-flattens all the arguments every time around.) If we prevent
unification with type families, then the solver happens to use the equality
before expanding the type family.
It would be lovely in the future to revisit this problem and remove this
extra, unnecessary check. But we retain it for now as it seems to work
better in practice.
Note [Refactoring hazard: checkTauTvUpdate]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I (Richard E.) have a sad story about refactoring this code, retained here
to prevent others (or a future me!) from falling into the same traps.
It all started with #11407, which was caused by the fact that the TyVarTy
case of defer_me didn't look in the kind. But it seemed reasonable to
simply remove the defer_me check instead.
It referred to two Notes (since removed) that were out of date, and the
fast_check code in occurCheckExpand seemed to do just about the same thing as
defer_me. The one piece that defer_me did that wasn't repeated by
occurCheckExpand was the type-family check. (See Note [Prevent unification
with type families].) So I checked the result of occurCheckExpand for any
type family occurrences and deferred if there were any. This was done
in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
This approach turned out not to be performant, because the expanded type
was bigger than the original type, and tyConsOfType looks through type
synonyms. So it then struck me that we could dispense with the defer_me
check entirely. This simplified the code nicely, and it cut the allocations
in T5030 by half. But, as documented in Note [Prevent unification with
type families], this destroyed performance in T3064. Regardless, I missed this
regression and the change was committed as
3f5d1a13f112f34d992f6b74656d64d95a3f506d .
Bottom lines:
* defer_me is back, but now fixed w.r.t. #11407.
* Tread carefully before you start to refactor here. There can be
lots of hard-to-predict consequences.
Note [Type synonyms and the occur check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally speaking we try to update a variable with type synonyms not
......
......@@ -275,4 +275,3 @@ test('T11361', normal, compile, ['-dunique-increment=-1'])
# -dunique-increment=-1 doesn't work inside the file
test('T11361a', normal, compile_fail, [''])
test('T11581', normal, compile, [''])
test('T7788', normal, compile, [''])
......@@ -31,13 +31,14 @@ T2693.hs:19:23: error:
In the expression: fst x + snd x
• Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
T2693.hs:30:47: error:
T2693.hs:29:20: error:
• Couldn't match type ‘TFn a0’ with ‘PVR a1’
Expected type: [PVR a1]
Actual type: [TFn a0]
Expected type: () -> Maybe (PVR a1)
Actual type: () -> Maybe (TFn a0)
The type variables ‘a0’, ‘a1’ are ambiguous
• In the second argument of ‘map’, namely ‘pvs’
In the second argument of ‘min’, namely ‘(map pvrX pvs)’
In the expression: (map pvrX pvs) `min` (map pvrX pvs)
• Relevant bindings include
pvs :: [TFn a0] (bound at T2693.hs:29:8)
• In the first argument of ‘mapM’, namely ‘g’
In a stmt of a 'do' block: pvs <- mapM g undefined
In the expression:
do { pvs <- mapM g undefined;
let n = (map pvrX pvs) `min` (map pvrX pvs);
undefined }
......@@ -2,10 +2,8 @@
T4179.hs:26:16: error:
• Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
with ‘A2 (FCon x)’
Expected type: x (A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x))))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
Expected type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (FCon x) -> A3 (FCon x)
Actual type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
......
T5439.hs:82:33: error:
• Couldn't match expected type ‘Attempt
(WaitOpResult (WaitOps rs))’
with actual type ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
• In the second argument of ‘($)’, namely
‘inj $ Failure (e :: SomeException)’
T5439.hs:82:28: error:
• Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’
with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
• In the first argument of ‘complete’, namely ‘ev’
In the expression: complete ev
In a stmt of a 'do' block:
c <- complete ev $ inj $ Failure (e :: SomeException)
In the expression:
do { c <- complete ev $ inj $ Failure (e :: SomeException);
return $ c || not first }
• Relevant bindings include
register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
(bound at T5439.hs:64:9)
......
T7354.hs:28:11: error:
• Occurs check: cannot construct the infinite type:
a ~ Prim [Base t a] (Base t a)
Expected type: a -> Base t a
Actual type: Prim [Base t a] (Base t a) -> Base t a
t1 ~ Base t (Prim [t1] t1)
Expected type: Prim [t1] t1 -> Base t (Prim [t1] t1)
Actual type: Prim [t1] t1 -> t1
• In the first argument of ‘ana’, namely ‘alg’
In the expression: ana alg
In an equation for ‘foo’: foo = ana alg
• Relevant bindings include foo :: a -> t (bound at T7354.hs:28:1)
• Relevant bindings include
foo :: Prim [t1] t1 -> t (bound at T7354.hs:28:1)
T7729.hs:36:25: error:
T7729.hs:36:14: error:
• Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
Expected type: BasePrimMonad m a -> BasePrimMonad (Rand m) a
Actual type: BasePrimMonad m a -> t0 (BasePrimMonad m) a
Expected type: t0 (BasePrimMonad m) a -> Rand m a
Actual type: BasePrimMonad (Rand m) a -> Rand m a
The type variable ‘t0’ is ambiguous
• In the second argument of ‘(.)’, namely ‘lift’
• In the first argument of ‘(.)’, namely ‘liftPrim
In the expression: liftPrim . lift
In an equation for ‘liftPrim’: liftPrim = liftPrim . lift
• Relevant bindings include
......
......@@ -11,18 +11,20 @@ T7786.hs:86:22: error:
Nil :: Sing xxx <- return
(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
T7786.hs:86:22: error:
T7786.hs:86:49: error:
• Couldn't match type ‘xxx’
with ‘Intersect (BuriedUnder sub k 'Empty) inv’
Expected type: Sing xxx
Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)
• When checking that the pattern signature: Sing xxx
fits the type of its context:
Sing (Intersect (BuriedUnder sub k 'Empty) inv)
In the pattern: Nil :: Sing xxx
• In the first argument of ‘return’, namely
‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
In a stmt of a 'do' block:
Nil :: Sing xxx <- return
(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
In the expression:
do { Nil :: Sing xxx <- return
(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
return $ Sub db k sub }
• Relevant bindings include
sub :: Database sub (bound at T7786.hs:86:13)
k :: Sing k (bound at T7786.hs:86:11)
......
T7788.hs:9:7: error:
• Reduction stack overflow; size = 201
When simplifying the following type: F (Id (Fix Id))
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: undefined
In an equation for ‘foo’: foo = undefined
......@@ -9,3 +9,16 @@ T9554.hs:11:9: error:
you're sure that type checking should terminate)
• In the expression: x
In an equation for ‘foo’: foo x = x
T9554.hs:13:17: error:
• Reduction stack overflow; size = 201
When simplifying the following type:
F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the first argument of ‘foo’, namely ‘Proxy’
In the expression: foo Proxy
In the expression:
case foo Proxy of { Proxy -> putStrLn "Made it!" }
T9662.hs:46:4: error:
T9662.hs:47:8: error:
• Couldn't match type ‘k’ with ‘Int’
‘k’ is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
at T9662.hs:44:9
Expected type: Shape (((sh :. k) :. m) :. n)
-> Shape (((sh :. m) :. n) :. k)
Actual type: Shape
Expected type: Exp (((sh :. m) :. n) :. k)
-> Exp (((sh :. m) :. n) :. k)
Actual type: Exp
(Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-> Shape
-> Exp
(Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
• In the expression:
• In the first argument of ‘backpermute’, namely
‘(modify
(atom :. atom :. atom :. atom)
(\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
In the expression:
backpermute
(modify
(atom :. atom :. atom :. atom)
......
......@@ -138,3 +138,4 @@ test('T10141', normal, compile_fail, [''])
test('T10817', normal, compile_fail, [''])
test('T10899', normal, compile_fail, [''])
test('T11136', normal, compile_fail, [''])
test('T7788', normal, compile_fail, [''])
......@@ -364,7 +364,7 @@ test('T5030',
# of family-applications leads to less sharing, I think
# 2015-07-11: 201882912 reason unknown
(wordsize(64), 342331936, 10)]),
(wordsize(64), 653710960, 10)]),
# Previously 530000000 (+/- 10%)
# 17/1/13: 602993184 (x86_64/Linux)
# (new demand analyser)
......@@ -382,7 +382,6 @@ test('T5030',
# of family-applications leads to less sharing, I think
# 2015-03-17 403932600 tweak to solver algorithm
# 2015-12-11 653710960 TypeInType (see #11196)
# 2016-03-14 342331936 unify type families eagerly
only_ways(['normal'])
],
......
......@@ -2,6 +2,6 @@
T9260.hs:12:8: error:
• Couldn't match type ‘2’ with ‘1’
Expected type: Fin 1
Actual type: Fin ((0 + 1) + 1)
Actual type: Fin (1 + 1)
• In the expression: Fsucc Fzero
In an equation for ‘test’: test = Fsucc Fzero
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