Commit 836f0e24 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Fix a bug in occurs checking

1. Trac #12593 exposed a long-standing bug in the occurs
   checking machinery.  When unifying two type variables
          a ~ b
   where a /= b, we were assuming that there could be
   no occurs-check error.  But there can: 'a' can occur
   in b's kind!  When the RHS was a non-tyvar we used
   occurCheckExpand, which /did/ look in kinds, but not
   when the RHS was a tyvar.

   This bug has been lurking ever since TypeInType, maybe
   longer.  And it was present both in TcUnify (the on-the-fly
   unifier), and in TcInteract.

   I ended up refactoring both so that the tyvar/tyvar
   path naturally goes through the same occurs-check as
   non-tyvar rhss.  It's simpler and more robust now.

   One good thing is that both unifiers now share
       TcType.swapOverVars
       TcType.canSolveByUnification
   previously they had different logic for the same goals

2. Fixing this bug exposed another!  In T11635 we end
   up unifying
   (alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
   Now that the occurs check is done for tyvars too, we
   look inside beta's kind.  And then reject the program
   becuase of the forall inside there.  But in fact that
   forall is fine -- it does not count as impredicative
   polymoprhism.   See Note [Checking for foralls]
   in TcType.

3. All this fuss around occurrence checking forced me
   to look at TcUnify.checkTauTvUpdate
          and TcType.occurCheckExpand
   There's a lot of duplication there, and I managed
   to elminate quite a bit of it. For example,
   checkTauTvUpdate called a local 'defer_me'; and then
   called occurCheckExpand, which then used a very
   similar 'fast_check'.

   Things are better, but there is more to do.

(cherry picked from commit 66a8c194)
parent 11f9bffb
......@@ -10,6 +10,7 @@ module TcCanonical(
#include "HsVersions.h"
import TcRnTypes
import TcUnify( swapOverTyVars )
import TcType
import Type
import TcFlatten
......@@ -22,7 +23,6 @@ import Coercion
import FamInstEnv ( FamInstEnvs )
import FamInst ( tcTopNormaliseNewTypeTF_maybe )
import Var
import Name( isSystemName )
import Outputable
import DynFlags( DynFlags )
import VarSet
......@@ -657,13 +657,13 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
`andWhenContinue` \ new_ev ->
can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
-- Type variable on LHS or RHS are last. We want only flat types sent
-- to canEqTyVar.
-- Type variable on LHS or RHS are last.
-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2
= canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2
can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _
= canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1
can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
= canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
= canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
-- We've flattened and the types don't match. Give up.
can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2
......@@ -1337,18 +1337,26 @@ canCFunEqCan ev fn tys fsk
, cc_tyargs = tys', cc_fsk = fsk }) } }
---------------------
canEqTyVar :: CtEvidence -> EqRel -> SwapFlag
-> TcTyVar -- already flat
-> TcType -- already flat
canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
-> EqRel -> SwapFlag
-> TcTyVar -> TcType -- lhs: already flat, not a cast
-> TcType -> TcType -- rhs: already flat, not a cast
-> TcS (StopOrContinue Ct)
-- A TyVar on LHS, but so far un-zonked
canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2
= do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped)
canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _
| tv1 == tv2
= canEqReflexive ev eq_rel ps_ty1
| swapOverTyVars tv1 tv2
= do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped)
-- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
-- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
-- Flatten the RHS less vigorously, to avoid gratuitous flattening
-- True <=> xi2 should not itself be a type-function application
; dflags <- getDynFlags
; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 }
canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2
= do { dflags <- getDynFlags
; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
canEqTyVar2 :: DynFlags
......@@ -1363,21 +1371,17 @@ canEqTyVar2 :: DynFlags
-- preserved as much as possible
canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
| Just (tv2, kco2) <- getCastedTyVar_maybe xi2
= canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
| OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check
-- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2'
-- to establish the invariant that a does not appear in the
-- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand;
-- see Note [Occurs check expansion] in TcType
= rewriteEqEvidence ev swapped xi1 xi2' co1 (mkTcReflCo role xi2')
-- Must do the occurs check even on tyvar/tyvar
-- equalities, in case have x ~ (y :: ..x...)
-- Trac #12593
= rewriteEqEvidence ev swapped xi1 xi2' co1 co2
`andWhenContinue` \ new_ev ->
homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' ->
CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
, cc_rhs = xi2'', cc_eq_rel = eq_rel }
| otherwise -- Occurs check error
| otherwise -- Occurs check error (or a forall)
= do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2)
; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
`andWhenContinue` \ new_ev ->
......@@ -1396,117 +1400,13 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-- canonical, and we might loop if we were to use it in rewriting.
else do { traceTcS "Occurs-check in representational equality"
(ppr xi1 $$ ppr xi2)
; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
where
role = eqRelRole eq_rel
xi1 = mkTyVarTy tv1
co1 = mkTcReflCo role xi1
co2 = mkTcReflCo role xi2
canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped)
-> EqRel
-> SwapFlag
-> TcTyVar -> TcTyVar -- tv1, tv2
-> Coercion -- the co in (rhs = tv2 |> co)
-> TcS (StopOrContinue Ct)
-- Both LHS and RHS rewrote to a type variable
-- See Note [Canonical orientation for tyvar/tyvar equality constraints]
canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2
| tv1 == tv2
= do { let mk_coh = case swapped of IsSwapped -> mkTcCoherenceLeftCo
NotSwapped -> mkTcCoherenceRightCo
; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2)
; stopWith ev "Equal tyvars" }
-- We don't do this any more
-- See Note [Orientation of equalities with fmvs] in TcFlatten
-- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2
-- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1
| swap_over = do_swap
| otherwise = no_swap
where
role = eqRelRole eq_rel
xi1 = mkTyVarTy tv1
co1 = mkTcReflCo role xi1
xi2 = mkTyVarTy tv2
co2 = mkTcReflCo role xi2 `mkTcCoherenceRightCo` kco2
no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2
do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1
canon_eq swapped tv1 ty1 ty2 co1 co2
-- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped)
-- co1 : xi1 ~ tv1
-- co2 : xi2 ~ tv2
= do { traceTcS "canEqTyVarTyVar"
(vcat [ ppr swapped
, ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
, ppr ty1 <+> dcolon <+> ppr (typeKind ty1)
, ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
, ppr co1 <+> dcolon <+> ppr (tcCoercionKind co1)
, ppr co2 <+> dcolon <+> ppr (tcCoercionKind co2) ])
; rewriteEqEvidence ev swapped ty1 ty2 co1 co2
`andWhenContinue` \ new_ev ->
homogeniseRhsKind new_ev eq_rel ty1 ty2 $ \new_new_ev ty2' ->
CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
, cc_rhs = ty2', cc_eq_rel = eq_rel } }
{- We don't do this any more
See Note [Orientation of equalities with fmvs] in TcFlatten
-- tv1 is the flatten meta-var
do_fmv swapped tv1 xi1 xi2 co1 co2
| same_kind
= canon_eq swapped tv1 xi1 xi2 co1 co2
| otherwise -- Presumably tv1 :: *, since it is a flatten meta-var,
-- at a kind that has some interesting sub-kind structure.
-- Since the two kinds are not the same, we must have
-- tv1 `subKind` tv2, which is the wrong way round
-- e.g. (fmv::*) ~ (a::OpenKind)
-- So make a new meta-var and use that:
-- fmv ~ (beta::*)
-- (a::OpenKind) ~ (beta::*)
= ASSERT2( k1_sub_k2,
ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$
ppr xi2 <+> dcolon <+> ppr (typeKind xi2) )
ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars
do { tv_ty <- newFlexiTcSTy (tyVarKind tv1)
; new_ev <- newWantedEvVarNC (ctEvLoc ev)
(mkPrimEqPredRole (eqRelRole eq_rel)
g tv_ty xi2)
; emitWorkNC [new_ev]
; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) }
-}
swap_over
-- If tv1 is touchable, swap only if tv2 is also
-- touchable and it's strictly better to update the latter
-- But see Note [Avoid unnecessary swaps]
| Just lvl1 <- metaTyVarTcLevel_maybe tv1
= case metaTyVarTcLevel_maybe tv2 of
Nothing -> False
Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True
| lvl1 `strictlyDeeperThan` lvl2 -> False
| otherwise -> nicer_to_update_tv2
-- So tv1 is not a meta tyvar
-- If only one is a meta tyvar, put it on the left
-- This is not because it'll be solved; but because
-- the floating step looks for meta tyvars on the left
| isMetaTyVar tv2 = True
-- So neither is a meta tyvar (including FlatMetaTv)
-- If only one is a flatten skolem, put it on the left
-- See Note [Eliminate flat-skols]
| not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True
| otherwise = False
nicer_to_update_tv2
= (isSigTyVar tv1 && not (isSigTyVar tv2))
|| (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1)))
-- | Solve a reflexive equality constraint
canEqReflexive :: CtEvidence -- ty ~ ty
-> EqRel
......
......@@ -584,7 +584,7 @@ deriveStandalone (L loc (DerivDecl deriv_ty overlap_mode))
, text "type:" <+> ppr inst_ty ]
; let bale_out msg = failWithTc (derivingThingErr False cls cls_tys
inst_ty deriv_strat msg)
inst_ty msg)
; case tcSplitTyConApp_maybe inst_ty of
Just (tc, tc_args)
......@@ -595,9 +595,6 @@ deriveStandalone (L loc (DerivDecl deriv_ty overlap_mode))
| isUnboxedTupleTyCon tc
-> bale_out $ unboxedTyConErr "tuple"
| isUnboxedSumTyCon tc
-> bale_out $ unboxedTyConErr "sum"
| isAlgTyCon tc || isDataFamilyTyCon tc -- All other classes
-> do { spec <- mkEqnHelp (fmap unLoc overlap_mode)
tvs cls cls_tys tc tc_args
......
......@@ -13,6 +13,7 @@ import BasicTypes ( infinity, IntWithInf, intGtLimit )
import HsTypes ( HsIPName(..) )
import TcCanonical
import TcFlatten
import TcUnify( canSolveByUnification )
import VarSet
import Type
import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
......@@ -1121,56 +1122,33 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
; stopWith ev "Solved from inert (r)" }
| ReprEq <- eq_rel -- We never solve representational
= unsolved_inert -- equalities by unification
| isGiven ev -- See Note [Touchables and givens]
= unsolved_inert
| otherwise
= do { tclvl <- getTcLevel
; if canSolveByUnification tclvl ev eq_rel tv rhs
; if canSolveByUnification tclvl tv rhs
then do { solveByUnification ev tv rhs
; n_kicked <- kickOutAfterUnification tv
; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
else do { traceTcS "Can't solve tyvar equality"
(vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
, ppWhen (isMetaTyVar tv) $
nest 4 (text "TcLevel of" <+> ppr tv
<+> text "is" <+> ppr (metaTyVarTcLevel tv))
, text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
, text "TcLevel =" <+> ppr tclvl ])
; addInertEq workItem
; return (Stop ev (text "Kept as inert")) } }
interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
else unsolved_inert }
-- @trySpontaneousSolve wi@ solves equalities where one side is a
-- touchable unification variable.
-- Returns True <=> spontaneous solve happened
canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
-> TcTyVar -> Xi -> Bool
canSolveByUnification tclvl gw eq_rel tv xi
| ReprEq <- eq_rel -- we never solve representational equalities this way.
= False
| isGiven gw -- See Note [Touchables and givens]
= False
| isTouchableMetaTyVar tclvl tv
= case metaTyVarInfo tv of
SigTv -> is_tyvar xi
_ -> True
| otherwise -- Untouchable
= False
where
is_tyvar xi
= case tcGetTyVar_maybe xi of
Nothing -> False
Just tv -> case tcTyVarDetails tv of
MetaTv { mtv_info = info }
-> case info of
SigTv -> True
_ -> False
SkolemTv {} -> True
FlatSkol {} -> False
RuntimeUnk -> True
unsolved_inert
= do { traceTcS "Can't solve tyvar equality"
(vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
, ppWhen (isMetaTyVar tv) $
nest 4 (text "TcLevel of" <+> ppr tv
<+> text "is" <+> ppr (metaTyVarTcLevel tv))
, text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
; addInertEq workItem
; return (Stop ev (text "Kept as inert")) }
interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
-- Solve with the identity coercion
......@@ -1446,7 +1424,9 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty
; dischargeFmv old_ev fsk final_co alpha_ty
; traceTcS "doTopReactFunEq (occurs)" $
vcat [ text "old_ev:" <+> ppr old_ev
, nest 2 (text ":=") <+> ppr final_co
, nest 2 (text ":=") <+>
if isDerived old_ev then text "(derived)"
else ppr final_co
, text "new_ev:" <+> ppr new_ev ]
; stopWith old_ev "Fun/Top (wanted)" }
where
......
......@@ -83,6 +83,7 @@ module TcType (
---------------------------------
-- Misc type manipulators
deNoteType, occurCheckExpand, OccCheckResult(..),
occCheckExpand,
orphNamesOfType, orphNamesOfCo,
orphNamesOfTypes, orphNamesOfCoCon,
getDFunTyKey,
......@@ -1530,7 +1531,49 @@ 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
Note [Occurrence checking: look inside kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are considering unifying
(alpha :: *) ~ Int -> (beta :: alpha -> alpha)
This may be an error (what is that alpha doing inside beta's kind?),
but we must not make the mistake of actuallyy unifying or we'll
build an infinite data structure. So when looking for occurrences
of alpha in the rhs, we must look in the kinds of type variables
that occur there.
NB: we may be able to remove the problem via expansion; see
Note [Occurs check expansion]. So we have to try that.
Note [Checking for foralls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Unless we have -XImpredicativeTypes (which is a totally unsupported
feature), we do not want to unify
alpha ~ (forall a. a->a) -> Int
So we look for foralls hidden inside the type, and it's convenient
to do that at the same time as the occurs check (which looks for
occurrences of alpha).
However, it's not just a question of looking for foralls /anywhere/!
Consider
(alpha :: forall k. k->*) ~ (beta :: forall k. k->*)
This is legal; e.g. dependent/should_compile/T11635.
We don't want to reject it because of the forall in beta's kind,
but (see Note [Occurrence checking: look inside kinds]) we do
need to look in beta's kind. So we carry a flag saying if a 'forall'
is OK, and sitch the flag on when stepping inside a kind.
Why is it OK? Why does it not count as impredicative polymorphism?
The reason foralls are bad is because we reply on "seeing" foralls
when doing implicit instantiation. But the forall inside the kind is
fine. We'll generate a kind equality constraint
(forall k. k->*) ~ (forall k. k->*)
to check that the kinds of lhs and rhs are compatible. If alpha's
kind had instead been
(alpha :: kappa)
then this kind equality would rightly complain about unifying kappa
with (forall k. k->*)
-}
data OccCheckResult a
......@@ -1569,39 +1612,63 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
-- - TcUnify.checkTauTvUpdate (on-the-fly unifier)
-- - TcInteract.canSolveByUnification (main constraint solver)
occurCheckExpand dflags tv ty
| fast_check ty = return ty
| otherwise = go emptyVarEnv ty
= case fast_check impredicative ty of
OC_OK _ -> OC_OK ty
OC_Forall -> OC_Forall
OC_Occurs -> case occCheckExpand tv ty of
Nothing -> OC_Occurs
Just ty' -> OC_OK ty'
where
details = tcTyVarDetails tv
details = tcTyVarDetails tv
impredicative = canUnifyWithPolyType dflags details
-- 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 (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)
= impredicative
&& fast_check (tyVarKind tv')
&& (tv == tv' || fast_check ty)
fast_check (CastTy ty co) = fast_check ty && fast_check_co co
fast_check (CoercionTy co) = fast_check_co co
ok :: OccCheckResult ()
ok = OC_OK ()
fast_check :: Bool -> TcType -> OccCheckResult ()
-- True <=> Foralls are ok; otherwise stop with OC_Forall
-- See Note [Checking for foralls]
fast_check _ (TyVarTy tv')
| tv == tv' = OC_Occurs
| otherwise = fast_check True (tyVarKind tv')
-- See Note [Occurrence checking: look inside kinds]
fast_check b (TyConApp tc tys)
| not (b || isTauTyCon tc) = OC_Forall
| otherwise = mapM (fast_check b) tys >> ok
fast_check _ (LitTy {}) = ok
fast_check b (ForAllTy (Anon a) r) = fast_check b a >> fast_check b r
fast_check b (AppTy fun arg) = fast_check b fun >> fast_check b arg
fast_check b (CastTy ty co) = fast_check b ty >> fast_check_co co
fast_check _ (CoercionTy co) = fast_check_co co
fast_check b (ForAllTy (Named tv' _) ty)
| not b = OC_Forall
| tv == tv' = ok
| otherwise = do { fast_check True (tyVarKind tv')
; fast_check b ty }
-- we really are only doing an occurs check here; no bother about
-- impredicativity in coercions, as they're inferred
fast_check_co co = not (tv `elemVarSet` tyCoVarsOfCo co)
fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
| otherwise = ok
go :: VarEnv TyVar -- carries mappings necessary because of kind expansion
-> Type -> OccCheckResult Type
occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
occCheckExpand tv ty
= go emptyVarEnv ty
where
go :: VarEnv TyVar -> Type -> Maybe Type
-- The Varenv carries mappings necessary
-- because of kind expansion
go env (TyVarTy tv')
| tv == tv' = OC_Occurs
| tv == tv' = Nothing
| Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
| otherwise = do { k' <- go env (tyVarKind tv')
; return (mkTyVarTy $
setTyVarKind tv' k') }
-- See Note [Occurrence checking: look inside kinds]
go _ ty@(LitTy {}) = return ty
go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
; ty2' <- go env ty2
......@@ -1611,29 +1678,22 @@ occurCheckExpand dflags tv ty
; ty2' <- go env ty2
; return (mkFunTy ty1' ty2') }
go env ty@(ForAllTy (Named tv' vis) body_ty)
| not impredicative = OC_Forall
| tv == tv' = return ty
| otherwise = do { ki' <- go env ki
| otherwise = do { ki' <- go env (tyVarKind tv')
; let tv'' = setTyVarKind tv' ki'
env' = extendVarEnv env tv' tv''
; body' <- go env' body_ty
; return (ForAllTy (Named tv'' vis) body') }
where ki = tyVarKind tv'
-- For a type constructor application, first try expanding away the
-- offending variable from the arguments. If that doesn't work, next
-- see if the type constructor is a type synonym, and if so, expand
-- it and try again.
go env ty@(TyConApp tc tys)
= case do { tys <- mapM (go env) tys
; return (mkTyConApp tc tys) } of
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' <- coreView ty -> go env ty'
| otherwise -> bad
= case mapM (go env) tys of
Just tys' -> return (mkTyConApp tc tys')
Nothing | Just ty' <- coreView ty -> go env ty'
| otherwise -> Nothing
-- Failing that, try to expand a synonym
go env (CastTy ty co) = do { ty' <- go env ty
......@@ -1651,7 +1711,6 @@ occurCheckExpand dflags tv ty
; arg' <- go_co env arg
; return (mkAppCo co' arg') }
go_co env co@(ForAllCo tv' kind_co body_co)
| not impredicative = OC_Forall
| tv == tv' = return co
| otherwise = do { kind_co' <- go_co env kind_co
; let tv'' = setTyVarKind tv' $
......
......@@ -18,6 +18,7 @@ module TcUnify (
-- Various unifications
unifyType_, unifyType, unifyTheta, unifyKind, noThing,
uType, unifyExpType,
swapOverTyVars, canSolveByUnification,
--------------------------------
-- Holes
......@@ -1121,13 +1122,13 @@ uType origin t_or_k orig_ty1 orig_ty2
; case lookup_res of
Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
; go ty1 ty2 }
Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 }
Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
go ty1 (TyVarTy tv2)
= do { lookup_res <- lookupTcTyVar tv2
; case lookup_res of
Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
; go ty1 ty2 }
Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 }
Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
-- See Note [Expanding synonyms during unification]
go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
......@@ -1309,87 +1310,77 @@ of the substitution; rather, notice that @uVar@ (defined below) nips
back into @uTys@ if it turns out that the variable is already bound.
-}
----------
uUnfilledVar :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTauType -- Type 2
-> TcTyVar -- Tyvar 1
-> TcTauType -- Type 2
-> TcM Coercion
-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
-- It might be a skolem, or untouchable, or meta
uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable => no-op
= return (mkNomReflCo (mkTyVarTy tv1))
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
; case lookup2 of
Filled ty2'
-> uUnfilledVar origin t_or_k swapped tv1 details1 ty2'
Unfilled details2
-> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2
}
uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2
-- ty2 is not a type variable
= case details1 of
MetaTv { mtv_ref = ref1 }
-> do { dflags <- getDynFlags
; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2
; case mb_ty2' of
Just (ty2', co_k) -> maybe_sym swapped <$>
updateMeta tv1 ref1 ty2' co_k
Nothing -> do { traceTc "Occ/type-family defer"
(ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
$$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2))
; defer }
}
_other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
uUnfilledVar origin t_or_k swapped tv1 ty2
= do { ty2 <- zonkTcType ty2
-- Zonk to expose things to the
-- occurs check, and so that if ty2
-- looks like a type variable then it
-- is a type variable
; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
----------
uUnfilledVar1 :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar -- Tyvar 1
-> TcTauType -- Type 2, zonked
-> TcM Coercion
uUnfilledVar1 origin t_or_k swapped tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2
= go tv2
| otherwise
= uUnfilledVar2 origin t_or_k swapped tv1 ty2
where
defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2
-- Occurs check or an untouchable: just defer
-- NB: occurs check isn't necessarily fatal:
-- eg tv1 occured in type family parameter
-- 'go' handles the case where both are
-- tyvars so we might want to swap
go tv2 | tv1 == tv2 -- Same type variable => no-op
= return (mkNomReflCo (mkTyVarTy tv1))
----------------
uUnfilledVars :: CtOrigin
| swapOverTyVars tv1 tv2 -- Distinct type variables
= uUnfilledVar2 origin t_or_k (flipSwap swapped)
tv2 (mkTyVarTy tv1)