summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAustin Seipp <austin@well-typed.com>2014-09-25 23:06:19 -0500
committerAustin Seipp <austin@well-typed.com>2014-09-25 23:06:35 -0500
commit18155ac21257316b430bfa209512d06822319707 (patch)
treeb35acf2c50a3a6c4ef19422c194a522b815a767b
parenta3dcaa5382f47d8982038aaf6a177f56fe403339 (diff)
downloadhaskell-18155ac21257316b430bfa209512d06822319707.tar.gz
[ci skip] typecheck: detabify/dewhitespace TcUnify
Signed-off-by: Austin Seipp <austin@well-typed.com>
-rw-r--r--compiler/typecheck/TcUnify.lhs298
1 files changed, 146 insertions, 152 deletions
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index f943ccd663..d26091728e 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -7,21 +7,15 @@ Type subsumption and unification
\begin{code}
{-# LANGUAGE CPP #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and
--- detab the module (please do the detabbing in a separate patch). See
--- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
--- for details
module TcUnify (
-- Full-blown subsumption
- tcWrapResult, tcSubType, tcGen,
- checkConstraints, newImplication,
+ tcWrapResult, tcSubType, tcGen,
+ checkConstraints, newImplication,
-- Various unifications
- unifyType, unifyTypeList, unifyTheta,
- unifyKindX,
+ unifyType, unifyTypeList, unifyTheta,
+ unifyKindX,
--------------------------------
-- Holes
@@ -29,7 +23,7 @@ module TcUnify (
matchExpectedListTy,
matchExpectedPArrTy,
matchExpectedTyConApp,
- matchExpectedAppTy,
+ matchExpectedAppTy,
matchExpectedFunTys,
matchExpectedFunKind,
wrapFunResCoercion
@@ -100,32 +94,32 @@ thing_inside, and returns a wrapper to coerce between the two types
It's used wherever a language construct must have a functional type,
namely:
- A lambda expression
- A function definition
+ A lambda expression
+ A function definition
An operator section
This is not (currently) where deep skolemisation occurs;
-matchExpectedFunTys does not skolmise nested foralls in the
+matchExpectedFunTys does not skolmise nested foralls in the
expected type, because it expects that to have been done already
\begin{code}
-matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
- -> Arity
- -> TcRhoType
+matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
+ -> Arity
+ -> TcRhoType
-> TcM (TcCoercion, [TcSigmaType], TcRhoType)
-- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
-- then co : ty ~ (t1 -> ... -> tn -> ty_r)
--
--- Does not allocate unnecessary meta variables: if the input already is
--- a function, we just take it apart. Not only is this efficient,
+-- Does not allocate unnecessary meta variables: if the input already is
+-- a function, we just take it apart. Not only is this efficient,
-- it's important for higher rank: the argument might be of form
--- (forall a. ty) -> other
+-- (forall a. ty) -> other
-- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
-- hide the forall inside a meta-variable
-matchExpectedFunTys herald arity orig_ty
+matchExpectedFunTys herald arity orig_ty
= go arity orig_ty
where
-- If go n ty = (co, [t1,..,tn], ty_r)
@@ -145,19 +139,19 @@ matchExpectedFunTys herald arity orig_ty
go n_req ty@(TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
= do { cts <- readMetaTyVar tv
- ; case cts of
- Indirect ty' -> go n_req ty'
- Flexi -> defer n_req ty }
+ ; case cts of
+ Indirect ty' -> go n_req ty'
+ Flexi -> defer n_req ty }
-- In all other cases we bale out into ordinary unification
-- However unlike the meta-tyvar case, we are sure that the
- -- number of arrows doesn't match up, so we can add a bit
+ -- number of arrows doesn't match up, so we can add a bit
-- more context to the error message (cf Trac #7869)
go n_req ty = addErrCtxtM mk_ctxt $
defer n_req ty
------------
- defer n_req fun_ty
+ defer n_req fun_ty
= do { arg_tys <- newFlexiTyVarTys n_req openTypeKind
-- See Note [Foralls to left of arrow]
; res_ty <- newFlexiTyVarTy openTypeKind
@@ -173,10 +167,10 @@ matchExpectedFunTys herald arity orig_ty
; return (env', mk_msg orig_ty2 n_actual) }
mk_msg ty n_args
- = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
- sep [ptext (sLit "but its type") <+> quotes (pprType ty),
- if n_args == 0 then ptext (sLit "has none")
- else ptext (sLit "has only") <+> speakN n_args]
+ = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$
+ sep [ptext (sLit "but its type") <+> quotes (pprType ty),
+ if n_args == 0 then ptext (sLit "has none")
+ else ptext (sLit "has only") <+> speakN n_args]
\end{code}
Note [Foralls to left of arrow]
@@ -205,7 +199,7 @@ matchExpectedPArrTy exp_ty
----------------------
matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
- -> TcRhoType -- orig_ty
+ -> TcRhoType -- orig_ty
-> TcM (TcCoercion, -- T k1 k2 k3 a b c ~ orig_ty
[TcSigmaType]) -- Element types, k1 k2 k3 a b c
@@ -217,11 +211,11 @@ matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 ->
matchExpectedTyConApp tc orig_ty
= go orig_ty
where
- go ty
- | Just ty' <- tcView ty
+ go ty
+ | Just ty' <- tcView ty
= go ty'
- go ty@(TyConApp tycon args)
+ go ty@(TyConApp tycon args)
| tc == tycon -- Common case
= return (mkTcNomReflCo ty, args)
@@ -231,7 +225,7 @@ matchExpectedTyConApp tc orig_ty
; case cts of
Indirect ty -> go ty
Flexi -> defer }
-
+
go _ = defer
-- If the common case does not occur, instantiate a template
@@ -239,8 +233,8 @@ matchExpectedTyConApp tc orig_ty
-- Doing it this way ensures that the types we return are
-- kind-compatible with T. For example, suppose we have
-- matchExpectedTyConApp T (f Maybe)
- -- where data T a = MkT a
- -- Then we don't want to instantate T's data constructors with
+ -- where data T a = MkT a
+ -- Then we don't want to instantate T's data constructors with
-- (a::*) ~ Maybe
-- because that'll make types that are utterly ill-kinded.
-- This happened in Trac #7368
@@ -322,38 +316,38 @@ tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWra
-- Returns a wrapper of shape ty_actual ~ ty_expected
tcSubType origin ctxt ty_actual ty_expected
| isSigmaTy ty_actual
- = do { (sk_wrap, inst_wrap)
+ = do { (sk_wrap, inst_wrap)
<- tcGen ctxt ty_expected $ \ _ sk_rho -> do
{ (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
; 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
+ | 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 <- 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
+ -- 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
+ 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
; res <- tc_infer ty
- ; return (res, ty) }
+ ; return (res, ty) }
-----------------
tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId)
tcWrapResult expr actual_ty res_ty
= do { cow <- unifyType actual_ty res_ty
- -- Both types are deeply skolemised
+ -- Both types are deeply skolemised
; return (mkHsWrapCo cow expr) }
-----------------------------------
@@ -396,7 +390,7 @@ tcGen ctxt expected_ty thing_inside
text "expected_ty" <+> ppr expected_ty,
text "inst ty" <+> ppr tvs' <+> ppr rho' ]
- -- Generally we must check that the "forall_tvs" havn't been constrained
+ -- Generally we must check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- of the expected_ty. Here's an example:
-- runST (newVar True)
@@ -404,10 +398,10 @@ tcGen ctxt expected_ty thing_inside
-- for (newVar True), with s fresh. Then we unify with the runST's arg type
-- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
-- So now s' isn't unconstrained because it's linked to a.
- --
- -- However [Oct 10] now that the untouchables are a range of
+ --
+ -- However [Oct 10] now that the untouchables are a range of
-- TcTyVars, all this is handled automatically with no need for
- -- extra faffing around
+ -- extra faffing around
-- Use the *instantiated* type in the SkolemInfo
-- so that the names of displayed type variables line up
@@ -417,14 +411,14 @@ tcGen ctxt expected_ty thing_inside
thing_inside tvs' rho'
; return (wrap <.> mkWpLet ev_binds, result) }
- -- The ev_binds returned by checkConstraints is very
- -- often empty, in which case mkWpLet is a no-op
+ -- The ev_binds returned by checkConstraints is very
+ -- often empty, in which case mkWpLet is a no-op
checkConstraints :: SkolemInfo
- -> [TcTyVar] -- Skolems
- -> [EvVar] -- Given
- -> TcM result
- -> TcM (TcEvBinds, result)
+ -> [TcTyVar] -- Skolems
+ -> [EvVar] -- Given
+ -> TcM result
+ -> TcM (TcEvBinds, result)
checkConstraints skol_info skol_tvs given thing_inside
| null skol_tvs && null given
@@ -436,34 +430,34 @@ checkConstraints skol_info skol_tvs given thing_inside
= newImplication skol_info skol_tvs given thing_inside
newImplication :: SkolemInfo -> [TcTyVar]
- -> [EvVar] -> TcM result
+ -> [EvVar] -> TcM result
-> TcM (TcEvBinds, result)
newImplication skol_info skol_tvs given thing_inside
= ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
- do { ((result, untch), wanted) <- captureConstraints $
+ do { ((result, untch), wanted) <- captureConstraints $
captureUntouchables $
thing_inside
; if isEmptyWC wanted && null given
- -- Optimisation : if there are no wanteds, and no givens
- -- don't generate an implication at all.
- -- Reason for the (null given): we don't want to lose
+ -- Optimisation : if there are no wanteds, and no givens
+ -- don't generate an implication at all.
+ -- Reason for the (null given): we don't want to lose
-- the "inaccessible alternative" error check
- then
+ then
return (emptyTcEvBinds, result)
else do
{ ev_binds_var <- newTcEvBinds
; env <- getLclEnv
; emitImplication $ Implic { ic_untch = untch
- , ic_skols = skol_tvs
+ , ic_skols = skol_tvs
, ic_fsks = []
, ic_no_eqs = False
- , ic_given = given
+ , ic_given = given
, ic_wanted = wanted
, ic_insol = insolubleWC wanted
, ic_binds = ev_binds_var
- , ic_env = env
+ , ic_env = env
, ic_info = skol_info }
; return (TcEvBinds ev_binds_var, result) } }
@@ -515,7 +509,7 @@ unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2
%************************************************************************
%* *
- uType and friends
+ uType and friends
%* *
%************************************************************************
@@ -559,7 +553,7 @@ uType_defer origin ty1 ty2
-- unify_np (short for "no push" on the origin stack) does the work
uType origin orig_ty1 orig_ty2
= do { untch <- getUntouchables
- ; traceTc "u_tys " $ vcat
+ ; traceTc "u_tys " $ vcat
[ text "untch" <+> ppr untch
, sep [ ppr orig_ty1, text "~", ppr orig_ty2]
, ppr origin]
@@ -570,36 +564,36 @@ uType origin orig_ty1 orig_ty2
; return co }
where
go :: TcType -> TcType -> TcM TcCoercion
- -- The arguments to 'go' are always semantically identical
- -- to orig_ty{1,2} except for looking through type synonyms
+ -- The arguments to 'go' are always semantically identical
+ -- to orig_ty{1,2} except for looking through type synonyms
-- Variables; go for uVar
- -- Note that we pass in *original* (before synonym expansion),
- -- so that type variables tend to get filled in with
+ -- Note that we pass in *original* (before synonym expansion),
+ -- so that type variables tend to get filled in with
-- the most informative version of the type
- go (TyVarTy tv1) ty2
+ go (TyVarTy tv1) ty2
= do { lookup_res <- lookupTcTyVar tv1
; case lookup_res of
Filled ty1 -> go ty1 ty2
Unfilled ds1 -> uUnfilledVar origin NotSwapped tv1 ds1 ty2 }
- go ty1 (TyVarTy tv2)
+ go ty1 (TyVarTy tv2)
= do { lookup_res <- lookupTcTyVar tv2
; case lookup_res of
Filled ty2 -> go ty1 ty2
Unfilled ds2 -> uUnfilledVar origin IsSwapped tv2 ds2 ty1 }
-- See Note [Expanding synonyms during unification]
- --
- -- Also NB that we recurse to 'go' so that we don't push a
- -- new item on the origin stack. As a result if we have
- -- type Foo = Int
- -- and we try to unify Foo ~ Bool
- -- we'll end up saying "can't match Foo with Bool"
- -- rather than "can't match "Int with Bool". See Trac #4535.
+ --
+ -- Also NB that we recurse to 'go' so that we don't push a
+ -- new item on the origin stack. As a result if we have
+ -- type Foo = Int
+ -- and we try to unify Foo ~ Bool
+ -- we'll end up saying "can't match Foo with Bool"
+ -- rather than "can't match "Int with Bool". See Trac #4535.
go ty1 ty2
| Just ty1' <- tcView ty1 = go ty1' ty2
| Just ty2' <- tcView ty2 = go ty1 ty2'
-
+
-- Functions (or predicate functions) just check the two parts
go (FunTy fun1 arg1) (FunTy fun2 arg2)
= do { co_l <- uType origin fun1 fun2
@@ -607,11 +601,11 @@ uType origin orig_ty1 orig_ty2
; return $ mkTcFunCo Nominal co_l co_r }
-- Always defer if a type synonym family (type function)
- -- is involved. (Data families behave rigidly.)
+ -- is involved. (Data families behave rigidly.)
go ty1@(TyConApp tc1 _) ty2
- | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
+ | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2
go ty1 ty2@(TyConApp tc2 _)
- | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
+ | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-- See Note [Mismatched type lists and application decomposition]
@@ -623,24 +617,24 @@ uType origin orig_ty1 orig_ty2
| m == n
= return $ mkTcNomReflCo ty
- -- See Note [Care with type applications]
- -- Do not decompose FunTy against App;
+ -- See Note [Care with type applications]
+ -- Do not decompose FunTy against App;
-- it's often a type error, so leave it for the constraint solver
go (AppTy s1 t1) (AppTy s2 t2)
= go_app s1 t1 s2 t2
go (AppTy s1 t1) (TyConApp tc2 ts2)
| Just (ts2', t2') <- snocView ts2
- = ASSERT( isDecomposableTyCon tc2 )
+ = ASSERT( isDecomposableTyCon tc2 )
go_app s1 t1 (TyConApp tc2 ts2') t2'
- go (TyConApp tc1 ts1) (AppTy s2 t2)
+ go (TyConApp tc1 ts1) (AppTy s2 t2)
| Just (ts1', t1') <- snocView ts1
- = ASSERT( isDecomposableTyCon tc1 )
- go_app (TyConApp tc1 ts1') t1' s2 t2
+ = ASSERT( isDecomposableTyCon tc1 )
+ go_app (TyConApp tc1 ts1') t1' s2 t2
go ty1 ty2
- | tcIsForAllTy ty1 || tcIsForAllTy ty2
+ | tcIsForAllTy ty1 || tcIsForAllTy ty2
= unifySigmaTy origin ty1 ty2
-- Anything else fails
@@ -649,7 +643,7 @@ uType origin orig_ty1 orig_ty2
------------------
go_app s1 t1 s2 t2
= do { co_s <- uType origin s1 s2 -- See Note [Unifying AppTy]
- ; co_t <- uType origin t1 t2
+ ; co_t <- uType origin t1 t2
; return $ mkTcAppCo co_s co_t }
unifySigmaTy :: CtOrigin -> TcType -> TcType -> TcM TcCoercion
@@ -663,7 +657,7 @@ unifySigmaTy origin ty1 ty2
; let tys = mkTyVarTys skol_tvs
phi1 = Type.substTy subst1 body1
phi2 = Type.substTy (zipTopTvSubst tvs2 tys) body2
- skol_info = UnifyForAllSkol skol_tvs phi1
+ skol_info = UnifyForAllSkol skol_tvs phi1
; (ev_binds, co) <- checkConstraints skol_info skol_tvs [] $
uType origin phi1 phi2
@@ -683,27 +677,27 @@ so if one type is an App the other one jolly well better be too
Note [Unifying AppTy]
~~~~~~~~~~~~~~~~~~~~~
-Consider unifying (m Int) ~ (IO Int) where m is a unification variable
-that is now bound to (say) (Bool ->). Then we want to report
+Consider unifying (m Int) ~ (IO Int) where m is a unification variable
+that is now bound to (say) (Bool ->). Then we want to report
"Can't unify (Bool -> Int) with (IO Int)
-and not
+and not
"Can't unify ((->) Bool) with IO"
That is why we use the "_np" variant of uType, which does not alter the error
message.
Note [Mismatched type lists and application decomposition]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we find two TyConApps, you might think that the argument lists
+When we find two TyConApps, you might think that the argument lists
are guaranteed equal length. But they aren't. Consider matching
- w (T x) ~ Foo (T x y)
+ w (T x) ~ Foo (T x y)
We do match (w ~ Foo) first, but in some circumstances we simply create
a deferred constraint; and then go ahead and match (T x ~ T x y).
This came up in Trac #3950.
-So either
- (a) either we must check for identical argument kinds
+So either
+ (a) either we must check for identical argument kinds
when decomposing applications,
-
+
(b) or we must be prepared for ill-kinded unification sub-problems
Currently we adopt (b) since it seems more robust -- no need to maintain
@@ -762,7 +756,7 @@ back into @uTys@ if it turns out that the variable is already bound.
uUnfilledVar :: CtOrigin
-> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
- -> TcTauType -- Type 2
+ -> TcTauType -- Type 2
-> TcM TcCoercion
-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
-- It might be a skolem, or untouchable, or meta
@@ -774,7 +768,7 @@ uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
; case lookup2 of
- Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
+ Filled ty2' -> uUnfilledVar origin swapped tv1 details1 ty2'
Unfilled details2 -> uUnfilledVars origin swapped tv1 details1 tv2 details2
}
@@ -785,18 +779,18 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type varia
; mb_ty2' <- checkTauTvUpdate dflags tv1 non_var_ty2
; case mb_ty2' of
Just ty2' -> updateMeta tv1 ref1 ty2'
- Nothing -> do { traceTc "Occ/kind defer"
+ Nothing -> do { traceTc "Occ/kind 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
+ _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts
where
defer = unSwap swapped (uType_defer origin) (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
+ -- NB: occurs check isn't necessarily fatal:
+ -- eg tv1 occured in type family parameter
----------------
uUnfilledVars :: CtOrigin
@@ -813,7 +807,7 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
; mb_sub_kind <- unifyKindX k1 k2
; case mb_sub_kind of {
Nothing -> unSwap swapped (uType_defer origin) (mkTyVarTy tv1) ty2 ;
- Just sub_kind ->
+ Just sub_kind ->
case (sub_kind, details1, details2) of
-- k1 < k2, so update tv2
@@ -822,16 +816,16 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2
-- k2 < k1, so update tv1
(GT, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
- -- k1 = k2, so we are free to update either way
- (EQ, MetaTv { mtv_info = i1, mtv_ref = ref1 },
+ -- k1 = k2, so we are free to update either way
+ (EQ, MetaTv { mtv_info = i1, mtv_ref = ref1 },
MetaTv { mtv_info = i2, mtv_ref = ref2 })
| nicer_to_update_tv1 tv1 i1 i2 -> updateMeta tv1 ref1 ty2
| otherwise -> updateMeta tv2 ref2 ty1
(EQ, MetaTv { mtv_ref = ref1 }, _) -> updateMeta tv1 ref1 ty2
(EQ, _, MetaTv { mtv_ref = ref2 }) -> updateMeta tv2 ref2 ty1
- -- Can't do it in-place, so defer
- -- This happens for skolems of all sorts
+ -- Can't do it in-place, so defer
+ -- This happens for skolems of all sorts
(_, _, _) -> unSwap swapped (uType_defer origin) ty1 ty2 } }
where
k1 = tyVarKind tv1
@@ -854,9 +848,9 @@ checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType)
-- 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)
---
+--
-- We have two possible outcomes:
--- (1) Return the type to update the type variable with,
+-- (1) Return the type to update the type variable with,
-- [we know the update is ok]
-- (2) Return Nothing,
-- [the update might be dodgy]
@@ -882,16 +876,16 @@ checkTauTvUpdate dflags tv ty
Just LT -> return Nothing
_ | defer_me ty1 -- Quick test
-> -- Failed quick test so try harder
- case occurCheckExpand dflags tv ty1 of
+ 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
+ where
info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv
impredicative = xopt Opt_ImpredicativeTypes dflags
- || isOpenTypeKind (tyVarKind tv)
+ || isOpenTypeKind (tyVarKind tv)
-- Note [OpenTypeKind accepts foralls]
|| case info of { PolyTv -> True; _ -> False }
@@ -917,7 +911,7 @@ 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.
+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
@@ -945,7 +939,7 @@ solver gets to see, and hence simplify the type-function call, which
in turn might simplify the type of an inferred function. Test ghci046
is a case in point.
-More mysteriously, test T7010 gave a horrible error
+More mysteriously, test T7010 gave a horrible error
T7010.hs:29:21:
Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
Expected type: (ValueTuple Vector, ValueTuple Vector)
@@ -973,38 +967,38 @@ error. Consider:
x :: ()
x = f (\ x p -> p x)
-We will eventually get a constraint of the form t ~ A t. The ok function above will
+We will eventually get a constraint of the form t ~ A t. The ok function above will
properly expand the type (A t) to just (), which is ok to be unified with t. If we had
-unified with the original type A t, we would lead the type checker into an infinite loop.
+unified with the original type A t, we would lead the type checker into an infinite loop.
-Hence, if the occurs check fails for a type synonym application, then (and *only* then),
+Hence, if the occurs check fails for a type synonym application, then (and *only* then),
the ok function expands the synonym to detect opportunities for occurs check success using
-the underlying definition of the type synonym.
+the underlying definition of the type synonym.
-The same applies later on in the constraint interaction code; see TcInteract,
-function @occ_check_ok@.
+The same applies later on in the constraint interaction code; see TcInteract,
+function @occ_check_ok@.
-Note [Type family sharing]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must avoid eagerly unifying type variables to types that contain function symbols,
+Note [Type family sharing]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must avoid eagerly unifying type variables to types that contain function symbols,
because this may lead to loss of sharing, and in turn, in very poor performance of the
-constraint simplifier. Assume that we have a wanted constraint:
-{
- m1 ~ [F m2],
- m2 ~ [F m3],
- m3 ~ [F m4],
- D m1,
- D m2,
- D m3
-}
-where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
-then, after zonking, our constraint simplifier will be faced with the following wanted
-constraint:
-{
- D [F [F [F m4]]],
- D [F [F m4]],
- D [F m4]
-}
+constraint simplifier. Assume that we have a wanted constraint:
+{
+ m1 ~ [F m2],
+ m2 ~ [F m3],
+ m3 ~ [F m4],
+ D m1,
+ D m2,
+ D m3
+}
+where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
+then, after zonking, our constraint simplifier will be faced with the following wanted
+constraint:
+{
+ D [F [F [F m4]]],
+ D [F [F m4]],
+ D [F m4]
+}
which has to be flattened by the constraint solver. In the absence of
a flat-cache, this may generate a polynomially larger number of
flatten skolems and the constraint sets we are working with will be
@@ -1020,12 +1014,12 @@ sharing, so there's no great harm in losing it -- and it's generally
more efficient to do the unification up-front.
\begin{code}
-data LookupTyVarResult -- The result of a lookupTcTyVar call
- = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
+data LookupTyVarResult -- The result of a lookupTcTyVar call
+ = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv
| Filled TcType
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
-lookupTcTyVar tyvar
+lookupTcTyVar tyvar
| MetaTv { mtv_ref = ref } <- details
= do { meta_details <- readMutVar ref
; case meta_details of
@@ -1100,10 +1094,10 @@ Hence the isTcTyVar tests before calling lookupTcTyVar.
matchExpectedFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-matchExpectedFunKind (FunTy arg_kind res_kind)
+matchExpectedFunKind (FunTy arg_kind res_kind)
= return (Just (arg_kind,res_kind))
-matchExpectedFunKind (TyVarTy kvar)
+matchExpectedFunKind (TyVarTy kvar)
| isTcTyVar kvar, isMetaTyVar kvar
= do { maybe_kind <- readMetaTyVar kvar
; case maybe_kind of
@@ -1116,10 +1110,10 @@ matchExpectedFunKind (TyVarTy kvar)
matchExpectedFunKind _ = return Nothing
------------------
+-----------------
unifyKindX :: TcKind -- k1 (actual)
-> TcKind -- k2 (expected)
- -> TcM (Maybe Ordering)
+ -> TcM (Maybe Ordering)
-- Returns the relation between the kinds
-- Just LT <=> k1 is a sub-kind of k2
-- Nothing <=> incomparable