Commit 10f83429 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Do not instantiate unification variables with polytypes

Without -XImpredicativeTypes, the typing rules say that a function
should be instantiated only at a *monotype*.  In implementation terms,
that means that a unification variable should not unify with a type
involving foralls.  But we were not enforcing that rule, and that
gave rise to some confusing error messages, such as
  Trac #7264, #6069

This patch adds the test for foralls.  There are consequences

 * I put the test in occurCheckExpand, since that is where we see if a
   type can unify with a given unification variable.  So
   occurCheckExpand has to get DynFlags, so it can test for
   -XImpredicativeTypes

 * We want this to work
      foo :: (forall a. a -> a) -> Int
      foo = error "foo"
   But that means instantiating error at a polytype!  But error is special
   already because you can instantiate it at an unboxed type like Int#.
   So I extended the specialness to allow type variables of openTypeKind
   to unify with polytypes, regardless of -XImpredicativeTypes.

   Conveniently, this works in TcUnify.matchExpectedFunTys, which generates
   unification variable for the function arguments, which can be polymorphic.

 * GHC has a special typing rule for ($) (see Note [Typing rule
   for ($)] in TcExpr).  It unifies the argument and result with a
   unification variable to exclude unboxed types -- but that means I
   now need a kind of unificatdion variable that *can* unify with a
   polytype.

   So for this sole case I added PolyTv to the data type TcType.MetaInfo.
   I suspect we'll find mor uses for this, and the changes are tiny,
   but it still feel a bit of a hack.  Well the special rule for ($)
   is a hack!

There were some consequential changes in error reporting (TcErrors).
parent 4baebfae
......@@ -1150,17 +1150,12 @@ canEqLeafTyVarEq loc ev tv s2 -- ev :: tv ~ s2
setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
; return Stop } ;
(Just tv1', _) ->
(Just tv1', _) -> do
-- LHS rewrote to a type variable, RHS to something else
case occurCheckExpand tv1' xi2 of
Nothing -> -- Occurs check error
do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
; case mb of
Nothing -> return Stop
Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
Just xi2' -> -- No occurs check, so we can continue; but make sure
{ dflags <- getDynFlags
; case occurCheckExpand dflags tv1' xi2 of
OC_OK xi2' -> -- No occurs check, so we can continue; but make sure
-- that the new goal has enough type synonyms expanded by
-- by the occurCheckExpand
do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2') co
......@@ -1169,7 +1164,13 @@ canEqLeafTyVarEq loc ev tv s2 -- ev :: tv ~ s2
Just new_ev -> continueWith $
CTyEqCan { cc_ev = new_ev, cc_loc = loc
, cc_tyvar = tv1', cc_rhs = xi2' } }
} }
_bad -> -- Occurs check error
do { mb <- rewriteCtFlavor ev (mkTcEqPred xi1 xi2) co
; case mb of
Nothing -> return Stop
Just new_ev -> canEqFailure loc new_ev xi1 xi2 }
} } }
mkHdEqPred :: Type -> TcCoercion -> TcCoercion -> TcCoercion
-- Make a higher-dimensional equality
......
......@@ -548,7 +548,8 @@ mkEqErr1 ctxt ct
| isGiven ev
= do { (ctxt, binds_msg) <- relevantBindings ctxt ct
; let (given_loc, given_msg) = mk_given (cec_encl ctxt)
; mkEqErr_help ctxt (given_msg $$ binds_msg)
; dflags <- getDynFlags
; mkEqErr_help dflags ctxt (given_msg $$ binds_msg)
(ct { cc_loc = given_loc}) -- Note [Inaccessible code]
Nothing ty1 ty2 }
......@@ -556,7 +557,8 @@ mkEqErr1 ctxt ct
= do { (ctxt, binds_msg) <- relevantBindings ctxt ct
; (ctxt, tidy_orig) <- zonkTidyOrigin ctxt (ctLocOrigin (cc_loc ct))
; let (is_oriented, wanted_msg) = mk_wanted_extra tidy_orig
; mkEqErr_help ctxt (wanted_msg $$ binds_msg)
; dflags <- getDynFlags
; mkEqErr_help dflags ctxt (wanted_msg $$ binds_msg)
ct is_oriented ty1 ty2 }
where
ev = cc_ev ct
......@@ -587,45 +589,66 @@ mkEqErr1 ctxt ct
mk_wanted_extra _ = (Nothing, empty)
mkEqErr_help, reportEqErr
:: ReportErrCtxt -> SDoc
-> Ct
-> Maybe SwapFlag -- Nothing <=> not sure
-> TcType -> TcType -> TcM ErrMsg
mkEqErr_help ctxt extra ct oriented ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr ctxt extra ct oriented tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr ctxt extra ct swapped tv2 ty1
mkEqErr_help :: DynFlags -> ReportErrCtxt -> SDoc
-> Ct
-> Maybe SwapFlag -- Nothing <=> not sure
-> TcType -> TcType -> TcM ErrMsg
mkEqErr_help dflags ctxt extra ct oriented ty1 ty2
| Just tv1 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt extra ct swapped tv2 ty1
| otherwise = reportEqErr ctxt extra ct oriented ty1 ty2
where
swapped = fmap flipSwap oriented
reportEqErr :: ReportErrCtxt -> SDoc
-> Ct
-> Maybe SwapFlag -- Nothing <=> not sure
-> TcType -> TcType -> TcM ErrMsg
reportEqErr ctxt extra1 ct oriented ty1 ty2
= do { (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
; mkErrorMsg ctxt' ct (vcat [ misMatchOrCND ctxt' ct oriented ty1 ty2
, extra2, extra1]) }
mkTyVarEqErr :: ReportErrCtxt -> SDoc -> Ct -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> SDoc -> Ct
-> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-- Occurs check
| isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round; see TcCanonical.reOrient
|| isSigTyVar tv1 && not (isTyVarTy ty2)
mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
| isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would
-- be oriented the other way round; see TcCanonical.reOrient
= mkErrorMsg ctxt ct (vcat [ misMatchOrCND ctxt ct oriented ty1 ty2
, extraTyVarInfo ctxt ty1 ty2
, extra ])
-- So tv is a meta tyvar, and presumably it is
-- an *untouchable* meta tyvar, else it'd have been unified
-- So tv is a meta tyvar (or started that way before we
-- generalised it). So presumably it is an *untouchable*
-- meta tyvar or a SigTv, else it'd have been unified
| not (k2 `tcIsSubKind` k1) -- Kind error
= mkErrorMsg ctxt ct $ (kindErrorMsg (mkTyVarTy tv1) ty2 $$ extra)
| isNothing (occurCheckExpand tv1 ty2)
| OC_Occurs <- occ_check_expand
= do { let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:")
2 (sep [ppr ty1, char '~', ppr ty2])
; (ctxt', extra2) <- mkEqInfoMsg ctxt ct ty1 ty2
; mkErrorMsg ctxt' ct (occCheckMsg $$ extra2 $$ extra) }
| OC_Forall <- occ_check_expand
= do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
<+> quotes (ppr tv1)
, hang (ptext (sLit "with a type involving foralls:")) 2 (ppr ty2)
, nest 2 (ptext (sLit "Perhaps you want -XImpredicativeTypes")) ]
; mkErrorMsg ctxt ct msg }
-- If the immediately-enclosing implication has 'tv' a skolem, and
-- we know by now its an InferSkol kind of skolem, then presumably
-- it started life as a SigTv, else it'd have been unified.
-- So just report a mis-match here, without gettin into occurs-checks etc
| (implic:_) <- cec_encl ctxt
, Implic { ic_skols = skols } <- implic
, tv1 `elem` skols
= mkErrorMsg ctxt ct (vcat [ misMatchMsg oriented ty1 ty2
, extraTyVarInfo ctxt ty1 ty2
, extra ])
-- Check for skolem escape
| (implic:_) <- cec_encl ctxt -- Get the innermost context
, Implic { ic_env = env, ic_skols = skols, ic_info = skol_info } <- implic
......@@ -665,6 +688,7 @@ mkTyVarEqErr ctxt extra ct oriented tv1 ty2
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, becuase F is a type function.
where
occ_check_expand = occurCheckExpand dflags tv1 ty2
k1 = tyVarKind tv1
k2 = typeKind ty2
ty1 = mkTyVarTy tv1
......
......@@ -318,10 +318,13 @@ tcExpr (OpApp arg1 op fix arg2) res_ty
-- Make sure that the argument and result types have kind '*'
-- Eg we do not want to allow (D# $ 4.0#) Trac #5570
-- ($) :: forall ab. (a->b) -> a -> b
; a_ty <- newFlexiTyVarTy liftedTypeKind
; b_ty <- newFlexiTyVarTy liftedTypeKind
-- (which gives a seg fault)
-- We do this by unifying with a MetaTv; but of course
-- it must allow foralls in the type it unifies with (hence PolyTv)!
-- ($) :: forall ab. (a->b) -> a -> b
; a_ty <- newPolyFlexiTyVarTy
; b_ty <- newPolyFlexiTyVarTy
; arg2' <- tcArg op (arg2, arg2_ty, 2)
; co_res <- unifyType b_ty res_ty -- b ~ res
......
......@@ -67,14 +67,13 @@ import NameEnv
import TysWiredIn
import BasicTypes
import SrcLoc
import DynFlags ( ExtensionFlag( Opt_DataKinds ) )
import DynFlags ( ExtensionFlag( Opt_DataKinds ), getDynFlags )
import Unique
import UniqSupply
import Outputable
import FastString
import Util
import Data.Maybe
import Control.Monad ( unless, when, zipWithM )
import PrelNames( ipClassName, funTyConKey )
\end{code}
......@@ -1229,7 +1228,8 @@ Here
* Then unificaiton makes a_sig := a_sk
That's why we must make a_sig a SigTv, not a SkolemTv, so that it can unify to a_sk.
That's why we must make a_sig a MetaTv (albeit a SigTv),
not a SkolemTv, so that it can unify to a_sk.
For RULE binders, though, things are a bit different (yuk).
RULE "foo" forall (x::a) (y::[a]). f x y = ...
......@@ -1340,6 +1340,7 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
; act_kind <- zonkTcKind act_kind
; traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind $$ ppr exp_kind)
; env0 <- tcInitTidyEnv
; dflags <- getDynFlags
; let (exp_as, _) = splitKindFunTys exp_kind
(act_as, _) = splitKindFunTys act_kind
n_exp_as = length exp_as
......@@ -1351,12 +1352,16 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
occurs_check
| Just act_tv <- tcGetTyVar_maybe act_kind
= isNothing (occurCheckExpand act_tv exp_kind)
= check_occ act_tv exp_kind
| Just exp_tv <- tcGetTyVar_maybe exp_kind
= isNothing (occurCheckExpand exp_tv act_kind)
= check_occ exp_tv act_kind
| otherwise
= False
check_occ tv k = case occurCheckExpand dflags tv k of
OC_Occurs -> True
_bad -> False
err | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
= ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
<+> ptext (sLit "is unlifted")
......
......@@ -24,6 +24,7 @@ module TcMType (
newFlexiTyVar,
newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newPolyFlexiTyVarTy,
newMetaKindVar, newMetaKindVars, mkKindSigVar,
mkTcTyVarName, cloneMetaTyVar,
......@@ -318,8 +319,9 @@ newMetaTyVar meta_info kind
= do { uniq <- newUnique
; let name = mkTcTyVarName uniq s
s = case meta_info of
TauTv -> fsLit "t"
SigTv -> fsLit "a"
PolyTv -> fsLit "s"
TauTv -> fsLit "t"
SigTv -> fsLit "a"
; details <- newMetaDetails meta_info
; return (mkTcTyVar name kind details) }
......@@ -438,6 +440,10 @@ newFlexiTyVarTy kind = do
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
newPolyFlexiTyVarTy :: TcM TcType
newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
; return (TyVarTy tv) }
tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- Instantiate with META type variables
-- Note that this works for a sequence of kind and type
......
......@@ -74,7 +74,7 @@ module TcType (
---------------------------------
-- Misc type manipulators
deNoteType, occurCheckExpand,
deNoteType, occurCheckExpand, OccCheckResult(..),
orphNamesOfType, orphNamesOfDFunHead, orphNamesOfCo,
getDFunTyKey,
evVarPred_maybe, evVarPred,
......@@ -331,6 +331,8 @@ data MetaInfo
-- A TauTv is always filled in with a tau-type, which
-- never contains any ForAlls
| PolyTv -- Like TauTv, but can unify with a sigma-type
| SigTv -- A variant of TauTv, except that it should not be
-- unified with a type, only with a type variable
-- SigTvs are only distinguished to improve error messages
......@@ -488,8 +490,9 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_untch = untch })
= pp_info <> brackets (ppr untch)
where
pp_info = case info of
TauTv -> ptext (sLit "tau")
SigTv -> ptext (sLit "sig")
PolyTv -> ptext (sLit "poly")
TauTv -> ptext (sLit "tau")
SigTv -> ptext (sLit "sig")
pprUserTypeCtxt :: UserTypeCtxt -> SDoc
pprUserTypeCtxt (InfSigCtxt n) = ptext (sLit "the inferred type for") <+> quotes (ppr n)
......@@ -1187,57 +1190,98 @@ even though we could also expand F to get rid of b.
See also Note [Type synonyms and canonicalization] in TcCanonical
\begin{code}
occurCheckExpand :: TcTyVar -> Type -> Maybe Type
data OccCheckResult a
= OC_OK a
| OC_Forall
| OC_NonTyVar
| OC_Occurs
instance Monad OccCheckResult where
return x = OC_OK x
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]
-- 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
-- Check whether
-- a) the given variable occurs in the given type.
-- b) there is a forall in the type (unless we have -XImpredicativeTypes
-- or it's a PolyTv
-- c) if it's a SigTv, ty should be a tyvar
--
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), 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 dflags tv ty
| MetaTv { mtv_info = SigTv } <- details
= go_sig_tv ty
| fast_check ty = return ty
| otherwise = go ty
where
go t@(TyVarTy tv') | tv == tv' = Nothing
| otherwise = Just t
details = ASSERT2( isTcTyVar tv, ppr tv ) tcTyVarDetails tv
impredicative
= case details of
MetaTv { mtv_info = PolyTv } -> 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
-- Check 'ty' is a tyvar, or can be expanded into one
go_sig_tv ty@(TyVarTy {}) = OC_OK ty
go_sig_tv ty | Just ty' <- tcView ty = go_sig_tv ty'
go_sig_tv _ = OC_NonTyVar
-- True => fine
fast_check (LitTy {}) = True
fast_check (TyVarTy tv') = tv /= tv'
fast_check (TyConApp _ tys) = all fast_check tys
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
&& fast_check (tyVarKind tv')
&& (tv == tv' || fast_check ty)
go t@(TyVarTy tv') | tv == tv' = OC_Occurs
| otherwise = return 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
go ty@(ForAllTy tv' body_ty)
| not impredicative = OC_Forall
| not (fast_check (tyVarKind tv')) = OC_Occurs
-- 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
-- In principle fast_check might fail because of a for-all
-- but we don't yet have poly-kinded tyvars so I'm not
-- going to worry about that now
| tv == tv' = return ty
| otherwise = do { body' <- go body_ty
; return (ForAllTy tv' body') }
-- 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
-}
= do { tys <- mapM go tys; return (mkTyConApp tc tys) }
`firstJust` -- First try to eliminate the tyvar from the args
do { ty <- tcView ty; go ty }
-- Failing that, try to expand a synonym
= 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
bad | Just ty' <- tcView ty -> go ty'
| otherwise -> bad
-- Failing that, try to expand a synonym
\end{code}
%************************************************************************
......
......@@ -160,6 +160,7 @@ matchExpectedFunTys herald arity orig_ty
defer n_req fun_ty
= addErrCtxtM mk_ctxt $
do { arg_tys <- newFlexiTyVarTys n_req openTypeKind
-- See Note [Foralls to left of arrow]
; res_ty <- newFlexiTyVarTy openTypeKind
; co <- unifyType fun_ty (mkFunTys arg_tys res_ty)
; return (co, arg_tys, res_ty) }
......@@ -179,6 +180,14 @@ matchExpectedFunTys herald arity orig_ty
else ptext (sLit "has only") <+> speakN n_args]
\end{code}
Note [Foralls to left of arrow]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f (x :: forall a. a -> a) = x
We give 'f' the type (alpha -> beta), and then want to unify
the alpha with (forall a. a->a). We want to the arg and result
of (->) to have openTypeKind, and this also permits foralls, so
we are ok.
\begin{code}
----------------------
......@@ -317,15 +326,24 @@ tcSubType origin ctxt ty_actual ty_expected
= do { (sk_wrap, inst_wrap)
<- tcGen ctxt ty_expected $ \ _ sk_rho -> do
{ (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
; cow <- unifyType in_rho sk_rho
; cow <- unify in_rho sk_rho
; return (coToHsWrapper cow <.> in_wrap) }
; return (sk_wrap <.> inst_wrap) }
| otherwise -- Urgh! It seems deeply weird to have equality
-- when actual is not a polytype, and it makes a big
-- difference e.g. tcfail104
= do { cow <- unifyType ty_actual ty_expected
= do { cow <- unify ty_actual ty_expected
; return (coToHsWrapper cow) }
where
-- In the case of patterns we call tcSubType with (expected, actual)
-- rather than (actual, expected). To get error messages the
-- right way round we have to fiddle with the origin
unify ty1 ty2 = uType u_origin ty1 ty2
where
u_origin = case origin of
PatSigOrigin -> TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 }
_other -> TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 }
tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind
......@@ -763,8 +781,9 @@ uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type variable
= case details1 of
MetaTv { mtv_info = TauTv, mtv_ref = ref1 }
-> do { mb_ty2' <- checkTauTvUpdate tv1 non_var_ty2
MetaTv { mtv_ref = ref1 }
-> do { dflags <- getDynFlags
; mb_ty2' <- checkTauTvUpdate dflags tv1 non_var_ty2
; case mb_ty2' of
Just ty2' -> updateMeta tv1 ref1 ty2'
Nothing -> do { traceTc "Occ/kind defer"
......@@ -830,9 +849,9 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
-- type sig
----------------
checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
-- (checkTauTvUpdate tv ty)
-- We are about to update the TauTv tv with ty.
-- We are about to update the TauTv/PolyTv tv with ty.
-- Check (a) that tv doesn't occur in ty (occurs check)
-- (b) that kind(ty) is a sub-kind of kind(tv)
--
......@@ -851,7 +870,11 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
-- we return Nothing, leaving it to the later constraint simplifier to
-- sort matters out.
checkTauTvUpdate tv ty
checkTauTvUpdate dflags tv ty
| SigTv <- info
= ASSERT( not (isTyVarTy ty) )
return Nothing
| otherwise
= do { ty1 <- zonkTcType ty
; sub_k <- unifyKindX (tyVarKind tv) (typeKind ty1)
; case sub_k of
......@@ -859,12 +882,19 @@ checkTauTvUpdate tv ty
Just LT -> return Nothing
_ | defer_me ty1 -- Quick test
-> -- Failed quick test so try harder
case occurCheckExpand tv ty1 of
Nothing -> return Nothing
Just ty2 | defer_me ty2 -> return Nothing
| otherwise -> return (Just ty2)
case occurCheckExpand dflags tv ty1 of
OC_OK ty2 | defer_me ty2 -> return Nothing
| otherwise -> return (Just ty2)
_ -> return Nothing
| otherwise -> return (Just ty1) }
where
info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
impredicative = xopt Opt_ImpredicativeTypes dflags
|| isOpenTypeKind (tyVarKind tv)
-- Note [OpenTypeKind accepts foralls]
|| case info of { PolyTv -> True; _ -> False }
defer_me :: TcType -> Bool
-- Checks for (a) occurrence of tv
-- (b) type family applicatios
......@@ -874,9 +904,27 @@ checkTauTvUpdate tv ty
defer_me (TyConApp tc tys) = isSynFamilyTyCon tc || any defer_me tys
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) = defer_me 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
......@@ -1146,9 +1194,10 @@ uUnboundKVar kv1 non_var_k2
; let k2b = defaultKind k2a
-- MetaKindVars must be bound only to simple kinds
; case occurCheckExpand kv1 k2b of
Just k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
_ -> return Nothing }
; dflags <- getDynFlags
; case occurCheckExpand dflags kv1 k2b of
OC_OK k2c -> do { writeMetaTyVar kv1 k2c; return (Just EQ) }
_ -> return Nothing }
mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc)
mkKindErrorCtxt ty1 ty2 k1 k2 env0
......
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