Commit 05289c2a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Improve occurs-check error reporting (fix Trac #6123)

We were wrongly reporting (a ~ F a) as an occurs-check error
when F is a type function.
parent bc188bbd
......@@ -7,7 +7,7 @@
-- for details
module TcCanonical(
canonicalize, flatten, flattenMany,
canonicalize, flatten, flattenMany, occurCheckExpand,
FlattenMode (..),
StopOrContinue (..)
) where
......@@ -1290,8 +1290,8 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
return Stop
else do
-- Not reflexivity but maybe an occurs error
{ occ_check_result <- canOccursCheck fl tv xi2
; let xi2' = fromMaybe xi2 occ_check_result
{ let occ_check_result = occurCheckExpand tv xi2
xi2' = fromMaybe xi2 occ_check_result
not_occ_err = isJust occ_check_result
-- Delicate: don't want to cache as solved a constraint with occurs error!
......@@ -1307,28 +1307,20 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
canEqFailure d new_fl
Nothing -> return Stop
} }
-- See Note [Type synonyms and canonicalization].
-- Check whether the given variable occurs in the given type. We may
-- have needed to do some type synonym unfolding in order to get rid
-- of the variable, so we also return the unfolded 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.
--
-- Precondition: the two types are not equal (looking though synonyms)
canOccursCheck :: CtEvidence -> TcTyVar -> Xi -> TcS (Maybe Xi)
canOccursCheck _gw tv xi = return (expandAway tv xi)
\end{code}
@expandAway tv xi@ expands synonyms in xi just enough to get rid of
occurrences of tv, if that is possible; otherwise, it returns Nothing.
Note [Occurs check expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@occurCheckExpand tv xi@ expands synonyms in xi just enough to get rid
of occurrences of tv outside type function arguments, if that is
possible; otherwise, it returns Nothing.
For example, suppose we have
type F a b = [a]
Then
expandAway b (F Int b) = Just [Int]
occurCheckExpand b (F Int b) = Just [Int]
but
expandAway a (F a Int) = Nothing
occurCheckExpand a (F a Int) = Nothing
We don't promise to do the absolute minimum amount of expanding
necessary, but we try not to do expansions we don't need to. We
......@@ -1336,49 +1328,61 @@ prefer doing inner expansions first. For example,
type F a b = (a, Int, a, [a])
type G b = Char
We have
expandAway b (F (G b)) = F Char
occurCheckExpand b (F (G b)) = F Char
even though we could also expand F to get rid of b.
See also Note [Type synonyms and canonicalization].
\begin{code}
expandAway :: TcTyVar -> Xi -> Maybe Xi
expandAway tv t@(TyVarTy tv')
| tv == tv' = Nothing
| otherwise = Just t
expandAway tv xi
| not (tv `elemVarSet` tyVarsOfType xi) = Just xi
expandAway tv (AppTy ty1 ty2)
= do { ty1' <- expandAway tv ty1
; ty2' <- expandAway tv ty2
; return (mkAppTy ty1' ty2') }
-- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2
expandAway tv (FunTy ty1 ty2)
= do { ty1' <- expandAway tv ty1
; ty2' <- expandAway tv ty2
; return (mkFunTy ty1' ty2') }
-- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2
expandAway tv ty@(ForAllTy {})
= let (tvs,rho) = splitForAllTys ty
tvs_knds = map tyVarKind tvs
in if tv `elemVarSet` tyVarsOfTypes tvs_knds then
-- Can't expand away the kinds unless we create
-- fresh variables which we don't want to do at this point.
Nothing
else do { rho' <- expandAway tv rho
; return (mkForAllTys tvs rho') }
-- 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.
expandAway tv ty@(TyConApp tc tys)
= (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv)
expandAway _ xi@(LitTy {}) = return xi
occurCheckExpand :: TcTyVar -> Type -> Maybe Type
-- Check whether the given variable occurs in the given type. We may
-- have needed to do some type synonym unfolding in order to get rid
-- of the variable, so we also return the unfolded 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 tv ty
| not (tv `elemVarSet` tyVarsOfType ty) = Just ty
| otherwise = go ty
where
go t@(TyVarTy tv') | tv == tv' = Nothing
| otherwise = Just t
go ty@(LitTy {}) = return ty
go (AppTy ty1 ty2) = do { ty1' <- go ty1
; ty2' <- go ty2
; return (mkAppTy ty1' ty2') }
-- mkAppTy <$> go ty1 <*> go ty2
go (FunTy ty1 ty2) = do { ty1' <- go ty1
; ty2' <- go ty2
; return (mkFunTy ty1' ty2') }
-- mkFunTy <$> go ty1 <*> go ty2
go ty@(ForAllTy {})
| tv `elemVarSet` tyVarsOfTypes tvs_knds = Nothing
-- Can't expand away the kinds unless we create
-- fresh variables which we don't want to do at this point.
| otherwise = do { rho' <- go rho
; return (mkForAllTys tvs rho') }
where
(tvs,rho) = splitForAllTys ty
tvs_knds = map tyVarKind tvs
-- 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 ty@(TyConApp tc tys)
| isSynFamilyTyCon tc -- It's ok for tv to occur under a type family application
= return ty -- Eg. (a ~ F a) is not an occur-check error
-- NB This case can't occur during canonicalisation,
-- because the arg is a Xi-type, but can occur in the
-- call from TcErrors
| otherwise
= (mkTyConApp tc <$> mapM go tys) <|> (tcView ty >>= go)
\end{code}
Note [Type synonyms and canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We treat type synonym applications as xi types, that is, they do not
count as type function applications. However, we do need to be a bit
careful with type synonyms: like type functions they may not be
......
......@@ -17,6 +17,7 @@ module TcErrors(
#include "HsVersions.h"
import TcCanonical( occurCheckExpand )
import TcRnMonad
import TcMType
import TcType
......@@ -455,17 +456,20 @@ mkEqErr1 ctxt ct
msg = mkExpectedActualMsg exp act
mk_err ctxt1 _ = mkEqErr_help ctxt1 ct False ty1 ty2
mkEqErr_help :: ReportErrCtxt
-> Ct
-> Bool -- True <=> Types are correct way round;
-- report "expected ty1, actual ty2"
-- False <=> Just report a mismatch without orientation
-- The ReportErrCtxt has expected/actual
-> TcType -> TcType -> TcM ErrMsg
mkEqErr_help, reportEqErr
:: ReportErrCtxt
-> Ct
-> Bool -- True <=> Types are correct way round;
-- report "expected ty1, actual ty2"
-- False <=> Just report a mismatch without orientation
-- The ReportErrCtxt has expected/actual
-> TcType -> TcType -> TcM ErrMsg
mkEqErr_help ctxt ct oriented ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt ct oriented tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt ct oriented tv2 ty1
| otherwise -- Neither side is a type variable
| otherwise = reportEqErr ctxt ct oriented ty1 ty2
reportEqErr ctxt ct oriented ty1 ty2
= do { ctxt' <- mkEqInfoMsg ctxt ct ty1 ty2
; mkErrorReport ctxt' (misMatchOrCND ctxt' ct oriented ty1 ty2) }
......@@ -484,7 +488,7 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
= mkErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2)
-- Occurs check
| tv1 `elemVarSet` tyVarsOfType ty2
| isNothing (occurCheckExpand tv1 ty2)
= let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2
(sep [ppr ty1, char '=', ppr ty2])
in mkErrorReport ctxt occCheckMsg
......@@ -524,21 +528,10 @@ mkTyVarEqErr ctxt ct oriented tv1 ty2
; mkErrorReport (addExtraTyVarInfo ctxt ty1 ty2) (msg $$ nest 2 extra) }
| otherwise
= pprTrace "mkTyVarEqErr" (ppr tv1 $$ ppr ty2 $$ ppr (cec_encl ctxt)) $
panic "mkTyVarEqErr"
-- I don't think this should happen, and if it does I want to know
-- Trac #5130 happened because an actual type error was not
-- reported at all! So not reporting is pretty dangerous.
--
-- OLD, OUT OF DATE COMMENT
-- This can happen, by a recursive decomposition of frozen
-- occurs check constraints
-- Example: alpha ~ T Int alpha has frozen.
-- Then alpha gets unified to T beta gamma
-- So now we have T beta gamma ~ T Int (T beta gamma)
-- Decompose to (beta ~ Int, gamma ~ T beta gamma)
-- The (gamma ~ T beta gamma) is the occurs check, but
-- the (beta ~ Int) isn't an error at all. So return ()
= reportEqErr ctxt ct oriented (mkTyVarTy tv1) ty2
-- This *can* happen (Trac #6123, and test T2627b)
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, becuase F is a type function.
where
k1 = tyVarKind tv1
k2 = typeKind ty2
......
......@@ -593,6 +593,11 @@ solveWithIdentity :: SubGoalDepth
-- must work for Derived as well as Wanted
-- Returns: workItem where
-- workItem = the new Given constraint
--
-- NB: No need for an occurs check here, because solveWithIdentity always
-- arises from a CTyEqCan, a *canonical* constraint. Its invariants
-- say that in (a ~ xi), the type variable a does not appear in xi.
-- See TcRnTypes.Ct invariants.
solveWithIdentity d wd tv xi
= do { let tv_ty = mkTyVarTy tv
; traceTcS "Sneaky unification:" $
......
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