2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
15 unifyKind, unifyKinds, unifyOpenTypeKind,
18 Coercion, ExprCoFn, PatCoFn,
19 (<$>), (<.>), mkCoercion,
20 idCoercion, isIdCoercion
24 #include "HsVersions.h"
27 import HsSyn ( HsExpr(..) )
28 import TcHsSyn ( TypecheckedHsExpr, TcPat, mkHsLet )
29 import TypeRep ( Type(..), SourceType(..), TyNote(..),
30 openKindCon, typeCon )
32 import TcMonad -- TcType, amongst others
33 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
34 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
36 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
37 tcGetTyVar_maybe, tcGetTyVar,
38 mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy,
39 typeKind, tcSplitFunTy_maybe, mkForAllTys,
40 isHoleTyVar, isSkolemTyVar, isUserTyVar,
41 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
42 eqKind, openTypeKind, liftedTypeKind, isTypeKind,
43 hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
45 import qualified Type ( getTyVar_maybe )
46 import Inst ( LIE, emptyLIE, plusLIE,
47 newDicts, instToId, tcInstCall
49 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult,
50 newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
51 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
52 import TcSimplify ( tcSimplifyCheck )
53 import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
54 import TcEnv ( TcTyThing(..), tcGetGlobalTyVars, tcLEnvElts )
55 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
56 import PprType ( pprType )
57 import Id ( Id, mkSysLocal, idType )
58 import Var ( Var, varName, tyVarKind )
59 import VarSet ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
61 import Name ( isSystemName, getSrcLoc )
62 import ErrUtils ( Message )
63 import BasicTypes ( Boxity, Arity, isBoxed )
64 import Util ( equalLength )
65 import Maybe ( isNothing )
71 * A hole is always filled in with an ordinary type, not another hole.
73 %************************************************************************
75 \subsection{Subsumption}
77 %************************************************************************
79 All the tcSub calls have the form
81 tcSub expected_ty offered_ty
83 offered_ty <= expected_ty
85 That is, that a value of type offered_ty is acceptable in
86 a place expecting a value of type expected_ty.
88 It returns a coercion function
89 co_fn :: offered_ty -> expected_ty
90 which takes an HsExpr of type offered_ty into one of type
94 type TcHoleType = TcSigmaType -- Either a TcSigmaType,
97 tcSubExp :: TcHoleType -> TcSigmaType -> TcM (ExprCoFn, LIE)
98 tcSubOff :: TcSigmaType -> TcHoleType -> TcM (ExprCoFn, LIE)
99 tcSub :: TcSigmaType -> TcSigmaType -> TcM (ExprCoFn, LIE)
102 These two check for holes
105 tcSubExp expected_ty offered_ty
106 = checkHole expected_ty offered_ty tcSub
108 tcSubOff expected_ty offered_ty
109 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
111 -- checkHole looks for a hole in its first arg;
112 -- If so, and it is uninstantiated, it fills in the hole
113 -- with its second arg
114 -- Otherwise it calls thing_inside, passing the two args, looking
115 -- through any instantiated hole
117 checkHole (TyVarTy tv) other_ty thing_inside
119 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
121 Just ty -> thing_inside ty other_ty
122 Nothing -> putTcTyVar tv other_ty `thenNF_Tc_`
123 returnTc (idCoercion, emptyLIE)
125 checkHole ty other_ty thing_inside
126 = thing_inside ty other_ty
129 No holes expected now. Add some error-check context info.
132 tcSub expected_ty actual_ty
133 = traceTc (text "tcSub" <+> details) `thenNF_Tc_`
134 tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
135 (tc_sub expected_ty expected_ty actual_ty actual_ty)
137 details = vcat [text "Expected:" <+> ppr expected_ty,
138 text "Actual: " <+> ppr actual_ty]
141 tc_sub carries the types before and after expanding type synonyms
144 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
145 -> TcSigmaType -- ..and after
146 -> TcSigmaType -- actual_ty, before
147 -> TcSigmaType -- ..and after
148 -> TcM (ExprCoFn, LIE)
150 -----------------------------------
152 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
153 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
155 -----------------------------------
156 -- Generalisation case
157 -- actual_ty: d:Eq b => b->b
158 -- expected_ty: forall a. Ord a => a->a
159 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
161 -- It is essential to do this *before* the specialisation case
162 -- Example: f :: (Eq a => a->a) -> ...
163 -- g :: Ord b => b->b
166 tc_sub exp_sty expected_ty act_sty actual_ty
167 | isSigmaTy expected_ty
168 = tcGen expected_ty (tyVarsOfType actual_ty) (
169 -- It's really important to check for escape wrt the free vars of
170 -- both expected_ty *and* actual_ty
171 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
172 ) `thenTc` \ (gen_fn, co_fn, lie) ->
173 returnTc (gen_fn <.> co_fn, lie)
175 -----------------------------------
176 -- Specialisation case:
177 -- actual_ty: forall a. Ord a => a->a
178 -- expected_ty: Int -> Int
179 -- co_fn e = e Int dOrdInt
181 tc_sub exp_sty expected_ty act_sty actual_ty
182 | isSigmaTy actual_ty
183 = tcInstCall Rank2Origin actual_ty `thenNF_Tc` \ (inst_fn, lie1, body_ty) ->
184 tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie2) ->
185 returnTc (co_fn <.> mkCoercion inst_fn, lie1 `plusLIE` lie2)
187 -----------------------------------
190 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
191 = tcSub_fun exp_arg exp_res act_arg act_res
193 -----------------------------------
194 -- Type variable meets function: imitate
196 -- NB 1: we can't just unify the type variable with the type
197 -- because the type might not be a tau-type, and we aren't
198 -- allowed to instantiate an ordinary type variable with
201 -- NB 2: can we short-cut to an error case?
202 -- when the arg/res is not a tau-type?
203 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
205 -- is perfectly fine!
207 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
208 = ASSERT( not (isHoleTyVar tv) )
209 getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
211 Just ty -> tc_sub exp_sty exp_ty ty ty
212 Nothing -> imitateFun tv exp_sty `thenNF_Tc` \ (act_arg, act_res) ->
213 tcSub_fun exp_arg exp_res act_arg act_res
215 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
216 = ASSERT( not (isHoleTyVar tv) )
217 getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
219 Just ty -> tc_sub ty ty act_sty act_ty
220 Nothing -> imitateFun tv act_sty `thenNF_Tc` \ (exp_arg, exp_res) ->
221 tcSub_fun exp_arg exp_res act_arg act_res
223 -----------------------------------
225 -- If none of the above match, we revert to the plain unifier
226 tc_sub exp_sty expected_ty act_sty actual_ty
227 = uTys exp_sty expected_ty act_sty actual_ty `thenTc_`
228 returnTc (idCoercion, emptyLIE)
231 %************************************************************************
233 \subsection{Functions}
235 %************************************************************************
238 tcSub_fun exp_arg exp_res act_arg act_res
239 = tc_sub act_arg act_arg exp_arg exp_arg `thenTc` \ (co_fn_arg, lie1) ->
240 tc_sub exp_res exp_res act_res act_res `thenTc` \ (co_fn_res, lie2) ->
241 tcGetUnique `thenNF_Tc` \ uniq ->
243 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
244 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
245 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
246 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
247 coercion | isIdCoercion co_fn_arg,
248 isIdCoercion co_fn_res = idCoercion
249 | otherwise = mkCoercion co_fn
251 co_fn e = DictLam [arg_id]
252 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
253 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
254 -- HsVar arg_id :: HsExpr exp_arg
255 -- co_fn_arg $it :: HsExpr act_arg
256 -- HsApp e $it :: HsExpr act_res
257 -- co_fn_res $it :: HsExpr exp_res
259 returnTc (coercion, lie1 `plusLIE` lie2)
261 imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType)
263 = ASSERT( not (isHoleTyVar tv) )
264 -- NB: tv is an *ordinary* tyvar and so are the new ones
266 -- Check that tv isn't a type-signature type variable
267 -- (This would be found later in checkSigTyVars, but
268 -- we get a better error message if we do it here.)
269 checkTcM (not (isSkolemTyVar tv))
270 (failWithTcM (unifyWithSigErr tv ty)) `thenTc_`
272 newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
273 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
274 putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
275 returnNF_Tc (arg,res)
279 %************************************************************************
281 \subsection{Generalisation}
283 %************************************************************************
286 tcGen :: TcSigmaType -- expected_ty
287 -> TcTyVarSet -- Extra tyvars that the universally
288 -- quantified tyvars of expected_ty
289 -- must not be unified
290 -> (TcRhoType -> TcM (result, LIE)) -- spec_ty
291 -> TcM (ExprCoFn, result, LIE)
292 -- The expression has type: spec_ty -> expected_ty
294 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
295 -- If not, the call is a no-op
296 = tcInstType SigTv expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
298 -- Type-check the arg and unify with poly type
299 thing_inside phi_ty `thenTc` \ (result, lie) ->
301 -- Check that the "forall_tvs" havn't been constrained
302 -- The interesting bit here is that we must include the free variables
303 -- of the expected_ty. Here's an example:
304 -- runST (newVar True)
305 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
306 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
307 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
308 -- So now s' isn't unconstrained because it's linked to a.
309 -- Conclusion: include the free vars of the expected_ty in the
310 -- list of "free vars" for the signature check.
312 newDicts SignatureOrigin theta `thenNF_Tc` \ dicts ->
313 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) ->
316 zonkTcTyVars forall_tvs `thenNF_Tc` \ forall_tys ->
317 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
318 text "expected_ty" <+> ppr expected_ty,
319 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
320 text "free_tvs" <+> ppr free_tvs,
321 text "forall_tys" <+> ppr forall_tys]) `thenNF_Tc_`
324 checkSigTyVarsWrt free_tvs forall_tvs `thenTc` \ zonked_tvs ->
326 traceTc (text "tcGen:done") `thenNF_Tc_`
329 -- This HsLet binds any Insts which came out of the simplification.
330 -- It's a bit out of place here, but using AbsBind involves inventing
331 -- a couple of new names which seems worse.
332 dict_ids = map instToId dicts
333 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
335 returnTc (mkCoercion co_fn, result, free_lie)
337 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
338 sig_msg = ptext SLIT("When generalising the type of an expression")
343 %************************************************************************
345 \subsection{Coercion functions}
347 %************************************************************************
350 type Coercion a = Maybe (a -> a)
351 -- Nothing => identity fn
353 type ExprCoFn = Coercion TypecheckedHsExpr
354 type PatCoFn = Coercion TcPat
356 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
357 Nothing <.> Nothing = Nothing
358 Nothing <.> Just f = Just f
359 Just f <.> Nothing = Just f
360 Just f1 <.> Just f2 = Just (f1 . f2)
362 (<$>) :: Coercion a -> a -> a
366 mkCoercion :: (a -> a) -> Coercion a
367 mkCoercion f = Just f
369 idCoercion :: Coercion a
372 isIdCoercion :: Coercion a -> Bool
373 isIdCoercion = isNothing
376 %************************************************************************
378 \subsection[Unify-exported]{Exported unification functions}
380 %************************************************************************
382 The exported functions are all defined as versions of some
383 non-exported generic functions.
385 Unify two @TauType@s. Dead straightforward.
388 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
389 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
390 = -- The unifier should only ever see tau-types
391 -- (no quantification whatsoever)
392 ASSERT2( isTauTy ty1, ppr ty1 )
393 ASSERT2( isTauTy ty2, ppr ty2 )
394 tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
398 @unifyTauTyList@ unifies corresponding elements of two lists of
399 @TauType@s. It uses @uTys@ to do the real work. The lists should be
400 of equal length. We charge down the list explicitly so that we can
401 complain if their lengths differ.
404 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
405 unifyTauTyLists [] [] = returnTc ()
406 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
407 unifyTauTyLists tys1 tys2
408 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
411 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
412 all together. It is used, for example, when typechecking explicit
413 lists, when all the elts should be of the same type.
416 unifyTauTyList :: [TcTauType] -> TcM ()
417 unifyTauTyList [] = returnTc ()
418 unifyTauTyList [ty] = returnTc ()
419 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
423 %************************************************************************
425 \subsection[Unify-uTys]{@uTys@: getting down to business}
427 %************************************************************************
429 @uTys@ is the heart of the unifier. Each arg happens twice, because
430 we want to report errors in terms of synomyms if poss. The first of
431 the pair is used in error messages only; it is always the same as the
432 second, except that if the first is a synonym then the second may be a
433 de-synonym'd version. This way we get better error messages.
435 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
438 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
439 -- ty1 is the *expected* type
441 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
442 -- ty2 is the *actual* type
445 -- Always expand synonyms (see notes at end)
446 -- (this also throws away FTVs)
447 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
448 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
450 -- Variables; go for uVar
451 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
452 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
453 -- "True" means args swapped
456 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
457 | n1 == n2 = uTys t1 t1 t2 t2
458 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
459 | c1 == c2 = unifyTauTyLists tys1 tys2
460 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
461 | tc1 == tc2 = unifyTauTyLists tys1 tys2
463 -- Functions; just check the two parts
464 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
465 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
467 -- Type constructors must match
468 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
469 | con1 == con2 && equalLength tys1 tys2
470 = unifyTauTyLists tys1 tys2
472 | con1 == openKindCon
473 -- When we are doing kind checking, we might match a kind '?'
474 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
475 -- (CCallable Int) and (CCallable Int#) are both OK
476 = unifyOpenTypeKind ps_ty2
478 -- Applications need a bit of care!
479 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
480 -- NB: we've already dealt with type variables and Notes,
481 -- so if one type is an App the other one jolly well better be too
482 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
483 = case tcSplitAppTy_maybe ty2 of
484 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
485 Nothing -> unifyMisMatch ps_ty1 ps_ty2
487 -- Now the same, but the other way round
488 -- Don't swap the types, because the error messages get worse
489 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
490 = case tcSplitAppTy_maybe ty1 of
491 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
492 Nothing -> unifyMisMatch ps_ty1 ps_ty2
494 -- Not expecting for-alls in unification
495 -- ... but the error message from the unifyMisMatch more informative
496 -- than a panic message!
498 -- Anything else fails
499 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
505 If you are tempted to make a short cut on synonyms, as in this
509 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
510 -- NO = if (con1 == con2) then
511 -- NO -- Good news! Same synonym constructors, so we can shortcut
512 -- NO -- by unifying their arguments and ignoring their expansions.
513 -- NO unifyTauTypeLists args1 args2
515 -- NO -- Never mind. Just expand them and try again
519 then THINK AGAIN. Here is the whole story, as detected and reported
520 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
522 Here's a test program that should detect the problem:
526 x = (1 :: Bogus Char) :: Bogus Bool
529 The problem with [the attempted shortcut code] is that
533 is not a sufficient condition to be able to use the shortcut!
534 You also need to know that the type synonym actually USES all
535 its arguments. For example, consider the following type synonym
536 which does not use all its arguments.
541 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
542 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
543 would fail, even though the expanded forms (both \tr{Int}) should
546 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
547 unnecessarily bind \tr{t} to \tr{Char}.
549 ... You could explicitly test for the problem synonyms and mark them
550 somehow as needing expansion, perhaps also issuing a warning to the
555 %************************************************************************
557 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
559 %************************************************************************
561 @uVar@ is called when at least one of the types being unified is a
562 variable. It does {\em not} assume that the variable is a fixed point
563 of the substitution; rather, notice that @uVar@ (defined below) nips
564 back into @uTys@ if it turns out that the variable is already bound.
567 uVar :: Bool -- False => tyvar is the "expected"
568 -- True => ty is the "expected" thing
570 -> TcTauType -> TcTauType -- printing and real versions
573 uVar swapped tv1 ps_ty2 ty2
574 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
575 getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
577 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
578 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
579 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
581 -- Expand synonyms; ignore FTVs
582 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
583 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
586 -- The both-type-variable case
587 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
589 -- Same type variable => no-op
593 -- Distinct type variables
594 -- ASSERT maybe_ty1 /= Just
596 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
598 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
602 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
603 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
607 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
608 putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
613 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
614 -- Try to get rid of open type variables as soon as poss
616 nicer_to_update_tv2 = isUserTyVar tv1
617 -- Don't unify a signature type variable if poss
618 || isSystemName (varName tv2)
619 -- Try to update sys-y type variables in preference to sig-y ones
621 -- Second one isn't a type variable
622 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
623 = -- Check that tv1 isn't a type-signature type variable
624 checkTcM (not (isSkolemTyVar tv1))
625 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
627 -- Do the occurs check, and check that we are not
628 -- unifying a type variable with a polytype
629 -- Returns a zonked type ready for the update
630 checkValue tv1 ps_ty2 non_var_ty2 `thenTc` \ ty2 ->
632 -- Check that the kinds match
633 checkKinds swapped tv1 ty2 `thenTc_`
635 -- Perform the update
636 putTcTyVar tv1 ty2 `thenNF_Tc_`
641 checkKinds swapped tv1 ty2
642 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
643 -- ty2 has been zonked at this stage, which ensures that
644 -- its kind has as much boxity information visible as possible.
645 | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
648 -- Either the kinds aren't compatible
649 -- (can happen if we unify (a b) with (c d))
650 -- or we are unifying a lifted type variable with an
651 -- unlifted type: e.g. (id 3#) is illegal
652 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
656 (k1,k2) | swapped = (tk2,tk1)
657 | otherwise = (tk1,tk2)
663 checkValue tv1 ps_ty2 non_var_ty2
664 -- Do the occurs check, and check that we are not
665 -- unifying a type variable with a polytype
666 -- Return the type to update the type variable with, or fail
668 -- Basically we want to update tv1 := ps_ty2
669 -- because ps_ty2 has type-synonym info, which improves later error messages
674 -- f :: (A a -> a -> ()) -> ()
678 -- x = f (\ x p -> p x)
680 -- In the application (p x), we try to match "t" with "A t". If we go
681 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
682 -- an infinite loop later.
683 -- But we should not reject the program, because A t = ().
684 -- Rather, we should bind t to () (= non_var_ty2).
686 -- That's why we have this two-state occurs-check
687 = zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
688 case okToUnifyWith tv1 ps_ty2' of {
689 Nothing -> returnTc ps_ty2' ; -- Success
692 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
693 case okToUnifyWith tv1 non_var_ty2' of
694 Nothing -> -- This branch rarely succeeds, except in strange cases
695 -- like that in the example above
696 returnTc non_var_ty2'
698 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
701 data Problem = OccurCheck | NotMonoType
703 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
704 -- (okToUnifyWith tv ty) checks whether it's ok to unify
707 -- Just p => not ok, problem p
712 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
713 | otherwise = Nothing
714 ok (AppTy t1 t2) = ok t1 `and` ok t2
715 ok (FunTy t1 t2) = ok t1 `and` ok t2
716 ok (TyConApp _ ts) = oks ts
717 ok (ForAllTy _ _) = Just NotMonoType
718 ok (SourceTy st) = ok_st st
719 ok (NoteTy (FTVNote _) t) = ok t
720 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
721 -- Type variables may be free in t1 but not t2
722 -- A forall may be in t2 but not t1
724 oks ts = foldr (and . ok) Nothing ts
726 ok_st (ClassP _ ts) = oks ts
727 ok_st (IParam _ t) = ok t
728 ok_st (NType _ ts) = oks ts
731 Just p `and` m = Just p
734 %************************************************************************
736 \subsection[Unify-fun]{@unifyFunTy@}
738 %************************************************************************
740 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
741 creation of type variables.
743 * subFunTy is used when we might be faced with a "hole" type variable,
744 in which case we should create two new holes.
746 * unifyFunTy is used when we expect to encounter only "ordinary"
747 type variables, so we should create new ordinary type variables
750 subFunTy :: TcHoleType -- Fail if ty isn't a function type
751 -- If it's a hole, make two holes, feed them to...
752 -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside
753 -> TcM a -- and bind the function type to the hole
755 subFunTy ty@(TyVarTy tyvar) thing_inside
757 = -- This is the interesting case
758 getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
760 Just ty' -> subFunTy ty' thing_inside ;
763 newHoleTyVarTy `thenNF_Tc` \ arg_ty ->
764 newHoleTyVarTy `thenNF_Tc` \ res_ty ->
767 thing_inside arg_ty res_ty `thenTc` \ answer ->
769 -- Extract the answers
770 readHoleResult arg_ty `thenNF_Tc` \ arg_ty' ->
771 readHoleResult res_ty `thenNF_Tc` \ res_ty' ->
773 -- Write the answer into the incoming hole
774 putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenNF_Tc_`
776 -- And return the answer
779 subFunTy ty thing_inside
780 = unifyFunTy ty `thenTc` \ (arg,res) ->
784 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
785 -> TcM (TcType, TcType) -- otherwise return arg and result types
787 unifyFunTy ty@(TyVarTy tyvar)
788 = ASSERT( not (isHoleTyVar tyvar) )
789 getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
791 Just ty' -> unifyFunTy ty'
792 Nothing -> unify_fun_ty_help ty
795 = case tcSplitFunTy_maybe ty of
796 Just arg_and_res -> returnTc arg_and_res
797 Nothing -> unify_fun_ty_help ty
799 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
800 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
801 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
802 unifyTauTy ty (mkFunTy arg res) `thenTc_`
807 unifyListTy :: TcType -- expected list type
808 -> TcM TcType -- list element type
810 unifyListTy ty@(TyVarTy tyvar)
811 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
813 Just ty' -> unifyListTy ty'
814 other -> unify_list_ty_help ty
817 = case tcSplitTyConApp_maybe ty of
818 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
819 other -> unify_list_ty_help ty
821 unify_list_ty_help ty -- Revert to ordinary unification
822 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
823 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
826 -- variant for parallel arrays
828 unifyPArrTy :: TcType -- expected list type
829 -> TcM TcType -- list element type
831 unifyPArrTy ty@(TyVarTy tyvar)
832 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
834 Just ty' -> unifyPArrTy ty'
835 _ -> unify_parr_ty_help ty
837 = case tcSplitTyConApp_maybe ty of
838 Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnTc arg_ty
839 _ -> unify_parr_ty_help ty
841 unify_parr_ty_help ty -- Revert to ordinary unification
842 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
843 unifyTauTy ty (mkPArrTy elt_ty) `thenTc_`
848 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
849 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
850 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
852 Just ty' -> unifyTupleTy boxity arity ty'
853 other -> unify_tuple_ty_help boxity arity ty
855 unifyTupleTy boxity arity ty
856 = case tcSplitTyConApp_maybe ty of
857 Just (tycon, arg_tys)
859 && tyConArity tycon == arity
860 && tupleTyConBoxity tycon == boxity
862 other -> unify_tuple_ty_help boxity arity ty
864 unify_tuple_ty_help boxity arity ty
865 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
866 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
869 kind | isBoxed boxity = liftedTypeKind
870 | otherwise = openTypeKind
874 %************************************************************************
876 \subsection{Kind unification}
878 %************************************************************************
881 unifyKind :: TcKind -- Expected
885 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
888 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
889 unifyKinds [] [] = returnTc ()
890 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
892 unifyKinds _ _ = panic "unifyKinds: length mis-match"
896 unifyOpenTypeKind :: TcKind -> TcM ()
897 -- Ensures that the argument kind is of the form (Type bx)
898 -- for some boxity bx
900 unifyOpenTypeKind ty@(TyVarTy tyvar)
901 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
903 Just ty' -> unifyOpenTypeKind ty'
904 other -> unify_open_kind_help ty
907 | isTypeKind ty = returnTc ()
908 | otherwise = unify_open_kind_help ty
910 unify_open_kind_help ty -- Revert to ordinary unification
911 = newBoxityVar `thenNF_Tc` \ boxity ->
912 unifyKind ty (mkTyConApp typeCon [boxity])
916 %************************************************************************
918 \subsection[Unify-context]{Errors and contexts}
920 %************************************************************************
926 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
927 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
928 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
929 returnNF_Tc (err ty1' ty2')
934 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
935 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
938 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
940 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
941 -- tv1 is zonked already
942 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
943 returnNF_Tc (err ty2')
945 err ty2 = (env2, ptext SLIT("When matching types") <+>
946 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
948 (pp_expected, pp_actual) | swapped = (pp2, pp1)
949 | otherwise = (pp1, pp2)
950 (env1, tv1') = tidyOpenTyVar tidy_env tv1
951 (env2, ty2') = tidyOpenType env1 ty2
955 unifyMisMatch ty1 ty2
956 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
957 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
959 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
960 msg = hang (ptext SLIT("Couldn't match"))
961 4 (sep [quotes (ppr tidy_ty1),
962 ptext SLIT("against"),
963 quotes (ppr tidy_ty2)])
965 failWithTcM (env, msg)
967 unifyWithSigErr tyvar ty
968 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
969 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
971 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
972 (env2, tidy_ty) = tidyOpenType env1 ty
974 unifyCheck problem tyvar ty
976 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
978 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
979 (env2, tidy_ty) = tidyOpenType env1 ty
981 msg = case problem of
982 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
983 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
988 %************************************************************************
990 \subsection{Checking signature type variables}
992 %************************************************************************
994 @checkSigTyVars@ is used after the type in a type signature has been unified with
995 the actual type found. It then checks that the type variables of the type signature
997 (a) Still all type variables
998 eg matching signature [a] against inferred type [(p,q)]
999 [then a will be unified to a non-type variable]
1001 (b) Still all distinct
1002 eg matching signature [(a,b)] against inferred type [(p,p)]
1003 [then a and b will be unified together]
1005 (c) Not mentioned in the environment
1006 eg the signature for f in this:
1012 Here, f is forced to be monorphic by the free occurence of x.
1014 (d) Not (unified with another type variable that is) in scope.
1015 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1016 when checking the expression type signature, we find that
1017 even though there is nothing in scope whose type mentions r,
1018 nevertheless the type signature for the expression isn't right.
1020 Another example is in a class or instance declaration:
1022 op :: forall b. a -> b
1024 Here, b gets unified with a
1026 Before doing this, the substitution is applied to the signature type variable.
1028 We used to have the notion of a "DontBind" type variable, which would
1029 only be bound to itself or nothing. Then points (a) and (b) were
1030 self-checking. But it gave rise to bogus consequential error messages.
1033 f = (*) -- Monomorphic
1035 g :: Num a => a -> a
1038 Here, we get a complaint when checking the type signature for g,
1039 that g isn't polymorphic enough; but then we get another one when
1040 dealing with the (Num x) context arising from f's definition;
1041 we try to unify x with Int (to default it), but find that x has already
1042 been unified with the DontBind variable "a" from g's signature.
1043 This is really a problem with side-effecting unification; we'd like to
1044 undo g's effects when its type signature fails, but unification is done
1045 by side effect, so we can't (easily).
1047 So we revert to ordinary type variables for signatures, and try to
1048 give a helpful message in checkSigTyVars.
1051 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1052 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1054 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1055 checkSigTyVarsWrt extra_tvs sig_tvs
1056 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenNF_Tc` \ extra_tvs' ->
1057 check_sig_tyvars extra_tvs' sig_tvs
1060 :: TcTyVarSet -- Global type variables. The universally quantified
1061 -- tyvars should not mention any of these
1062 -- Guaranteed already zonked.
1063 -> [TcTyVar] -- Universally-quantified type variables in the signature
1064 -- Not guaranteed zonked.
1065 -> TcM [TcTyVar] -- Zonked signature type variables
1067 check_sig_tyvars extra_tvs []
1069 check_sig_tyvars extra_tvs sig_tvs
1070 = zonkTcTyVars sig_tvs `thenNF_Tc` \ sig_tys ->
1071 tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs ->
1073 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1075 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1076 text "gbl_tvs" <+> ppr gbl_tvs,
1077 text "extra_tvs" <+> ppr extra_tvs])) `thenNF_Tc_`
1079 checkTcM (allDistinctTyVars sig_tys env_tvs)
1080 (complain sig_tys env_tvs) `thenTc_`
1082 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
1085 complain sig_tys globals
1086 = -- "check" checks each sig tyvar in turn
1088 (env2, emptyVarEnv, [])
1089 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
1091 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1093 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1094 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1096 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1098 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1099 -- sig_tyvar is from the signature;
1100 -- ty is what you get if you zonk sig_tyvar and then tidy it
1102 -- acc maps a zonked type variable back to a signature type variable
1103 = case tcGetTyVar_maybe ty of {
1104 Nothing -> -- Error (a)!
1105 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1109 case lookupVarEnv acc tv of {
1110 Just sig_tyvar' -> -- Error (b)!
1111 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1113 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1117 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1118 -- The least comprehensible, so put it last
1120 -- get the local TcIds and TyVars from the environment,
1121 -- and pass them to find_globals (they might have tv free)
1122 then tcGetEnv `thenNF_Tc` \ ve ->
1123 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
1124 returnNF_Tc (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1127 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1133 -----------------------
1134 -- find_globals looks at the value environment and finds values
1135 -- whose types mention the offending type variable. It has to be
1136 -- careful to zonk the Id's type first, so it has to be in the monad.
1137 -- We must be careful to pass it a zonked type variable, too.
1142 -> NF_TcM (TidyEnv, [SDoc])
1144 find_globals tv tidy_env things
1145 = go tidy_env [] things
1147 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1148 go tidy_env acc (thing : things)
1149 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1151 Just d -> go tidy_env1 (d:acc) things
1152 Nothing -> go tidy_env1 acc things
1154 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1156 -----------------------
1157 find_thing ignore_it tidy_env (ATcId id)
1158 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1159 if ignore_it id_ty then
1160 returnNF_Tc (tidy_env, Nothing)
1162 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1163 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1164 nest 2 (parens (ptext SLIT("bound at") <+>
1165 ppr (getSrcLoc id)))]
1167 returnNF_Tc (tidy_env', Just msg)
1169 find_thing ignore_it tidy_env (ATyVar tv)
1170 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1171 if ignore_it tv_ty then
1172 returnNF_Tc (tidy_env, Nothing)
1174 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1175 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1176 msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
1178 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1179 | otherwise = equals <+> ppr tv_ty
1180 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1182 bound_at = tyVarBindingInfo tv
1184 returnNF_Tc (tidy_env2, Just msg)
1186 -----------------------
1187 escape_msg sig_tv tv globs
1188 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1189 if not (null globs) then
1190 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1191 nest 2 (vcat globs)]
1193 empty -- Sigh. It's really hard to give a good error message
1194 -- all the time. One bad case is an existential pattern match.
1195 -- We rely on the "When..." context to help.
1197 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1198 | otherwise = ptext SLIT("It")
1201 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1202 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1205 These two context are used with checkSigTyVars
1208 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1209 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1210 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1211 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1213 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1214 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1215 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1216 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1217 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1219 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
1222 returnNF_Tc (env3, msg)