Commit 073119e8 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Put the decision of when a unification variable can unify with a polytype

This was being doing independently in two places. Now it's done in one
place, TcType.canUnifyWithPolyType
parent b6855422
......@@ -41,6 +41,7 @@ module TcType (
metaTyVarUntouchables, setMetaTyVarUntouchables, metaTyVarUntouchables_maybe,
isTouchableMetaTyVar, isTouchableOrFmv,
isFloatedTouchableMetaTyVar,
canUnifyWithPolyType,
--------------------------------
-- Builders
......@@ -1202,16 +1203,7 @@ occurCheckExpand dflags tv ty
where
details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
impredicative
= case details of
MetaTv { mtv_info = ReturnTv } -> True
MetaTv { mtv_info = SigTv } -> False
MetaTv { mtv_info = TauTv } -> xopt Opt_ImpredicativeTypes dflags
|| isOpenTypeKind (tyVarKind tv)
-- Note [OpenTypeKind accepts foralls]
-- in TcUnify
_other -> True
-- We can have non-meta tyvars in given constraints
impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
-- Check 'ty' is a tyvar, or can be expanded into one
go_sig_tv ty@(TyVarTy {}) = OC_OK ty
......@@ -1259,8 +1251,36 @@ occurCheckExpand dflags tv ty
bad | Just ty' <- tcView ty -> go ty'
| otherwise -> bad
-- Failing that, try to expand a synonym
canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> TcKind -> Bool
canUnifyWithPolyType dflags details kind
= case details of
MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv]
MetaTv { mtv_info = SigTv } -> False
MetaTv { mtv_info = TauTv } -> xopt Opt_ImpredicativeTypes dflags
|| isOpenTypeKind kind
-- Note [OpenTypeKind accepts foralls]
_other -> True
-- We can have non-meta tyvars in given constraints
\end{code}
Note [OpenTypeKind accepts foralls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here is a common paradigm:
foo :: (forall a. a -> a) -> Int
foo = error "urk"
To make this work we need to instantiate 'error' with a polytype.
A similar case is
bar :: Bool -> (forall a. a->a) -> Int
bar True = \x. (x 3)
bar False = error "urk"
Here we need to instantiate 'error' with a polytype.
But 'error' has an OpenTypeKind type variable, precisely so that
we can instantiate it with Int#. So we also allow such type variables
to be instantiate with foralls. It's a bit of a hack, but seems
straightforward.
%************************************************************************
%* *
\subsection{Predicate types}
......
......@@ -1011,13 +1011,10 @@ checkTauTvUpdate dflags tv ty
_ -> return Nothing
| otherwise -> return (Just ty1) }
where
info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
-- See Note [ReturnTv] in TcType
details = ASSERT2( isMetaTyVar tv, ppr tv ) tcTyVarDetails tv
info = mtv_info details
is_return_tv = case info of { ReturnTv -> True; _ -> False }
impredicative = xopt Opt_ImpredicativeTypes dflags
|| isOpenTypeKind (tyVarKind tv)
-- Note [OpenTypeKind accepts foralls]
impredicative = canUnifyWithPolyType dflags details (tyVarKind tv)
defer_me :: TcType -> Bool
-- Checks for (a) occurrence of tv
......@@ -1031,23 +1028,6 @@ checkTauTvUpdate dflags tv ty
defer_me (ForAllTy _ ty) = not impredicative || defer_me ty
\end{code}
Note [OpenTypeKind accepts foralls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here is a common paradigm:
foo :: (forall a. a -> a) -> Int
foo = error "urk"
To make this work we need to instantiate 'error' with a polytype.
A similar case is
bar :: Bool -> (forall a. a->a) -> Int
bar True = \x. (x 3)
bar False = error "urk"
Here we need to instantiate 'error' with a polytype.
But 'error' has an OpenTypeKind type variable, precisely so that
we can instantiate it with Int#. So we also allow such type variables
to be instantiate with foralls. It's a bit of a hack, but seems
straightforward.
Note [Conservative unification check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When unifying (tv ~ rhs), w try to avoid creating deferred constraints
......
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