2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSub, tcGen, subFunTy,
10 checkSigTyVars, sigCtxt, sigPatCtxt,
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,
29 mkHsDictApp, mkHsTyApp, mkHsLet )
30 import TypeRep ( Type(..), SourceType(..), TyNote(..),
31 openKindCon, typeCon )
33 import TcMonad -- TcType, amongst others
34 import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType,
35 TcTyVarSet, TcThetaType,
37 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
38 tcGetTyVar_maybe, tcGetTyVar,
39 mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy,
40 typeKind, tcSplitFunTy_maybe, mkForAllTys,
41 isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars,
42 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
43 eqKind, openTypeKind, liftedTypeKind, isTypeKind,
44 hasMoreBoxityInfo, tyVarBindingInfo
46 import qualified Type ( getTyVar_maybe )
47 import Inst ( LIE, emptyLIE, plusLIE, mkLIE,
48 newDicts, instToId, tcInstCall
50 import TcMType ( getTcTyVar, putTcTyVar, tcInstType,
51 newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
52 zonkTcType, zonkTcTyVars, zonkTcTyVar )
53 import TcSimplify ( tcSimplifyCheck )
54 import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
55 import TcEnv ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts )
56 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
57 import PprType ( pprType )
58 import CoreFVs ( idFreeTyVars )
59 import Id ( mkSysLocal, idType )
60 import Var ( Var, varName, tyVarKind )
61 import VarSet ( elemVarSet, varSetElems )
63 import Name ( isSystemName, getSrcLoc )
64 import ErrUtils ( Message )
65 import BasicTypes ( Boxity, Arity, isBoxed )
66 import Util ( isSingleton, equalLength )
67 import Maybe ( isNothing )
72 %************************************************************************
74 \subsection{Subsumption}
76 %************************************************************************
79 tcSub :: TcSigmaType -- expected_ty; can be a type scheme;
80 -- can be a "hole" type variable
81 -> TcSigmaType -- actual_ty; can be a type scheme
82 -> TcM (ExprCoFn, LIE)
85 (tcSub expected_ty actual_ty) checks that
86 actual_ty <= expected_ty
87 That is, that a value of type actual_ty is acceptable in
88 a place expecting a value of type expected_ty.
90 It returns a coercion function
91 co_fn :: actual_ty -> expected_ty
92 which takes an HsExpr of type actual_ty into one of type
96 tcSub expected_ty actual_ty
97 = traceTc (text "tcSub" <+> details) `thenNF_Tc_`
98 tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
99 (tc_sub expected_ty expected_ty actual_ty actual_ty)
101 details = vcat [text "Expected:" <+> ppr expected_ty,
102 text "Actual: " <+> ppr actual_ty]
105 tc_sub carries the types before and after expanding type synonyms
108 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
109 -> TcSigmaType -- ..and after
110 -> TcSigmaType -- actual_ty, before
111 -> TcSigmaType -- ..and after
112 -> TcM (ExprCoFn, LIE)
114 -----------------------------------
116 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
117 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
119 -----------------------------------
120 -- "Hole type variable" case
121 -- Do this case before unwrapping for-alls in the actual_ty
123 tc_sub _ (TyVarTy tv) act_sty act_ty
125 = -- It's a "hole" type variable
126 getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
129 Just ty -> -- Already been assigned
130 tc_sub ty ty act_sty act_ty ;
132 Nothing -> -- Assign it
133 putTcTyVar tv act_sty `thenNF_Tc_`
134 returnTc (idCoercion, emptyLIE)
137 -----------------------------------
138 -- Generalisation case
139 -- actual_ty: d:Eq b => b->b
140 -- expected_ty: forall a. Ord a => a->a
141 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
143 -- It is essential to do this *before* the specialisation case
144 -- Example: f :: (Eq a => a->a) -> ...
145 -- g :: Ord b => b->b
148 tc_sub exp_sty expected_ty act_sty actual_ty
149 | isSigmaTy expected_ty
150 = tcGen expected_ty (
151 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
152 ) `thenTc` \ (gen_fn, co_fn, lie) ->
153 returnTc (gen_fn <.> co_fn, lie)
155 -----------------------------------
156 -- Specialisation case:
157 -- actual_ty: forall a. Ord a => a->a
158 -- expected_ty: Int -> Int
159 -- co_fn e = e Int dOrdInt
161 tc_sub exp_sty expected_ty act_sty actual_ty
162 | isSigmaTy actual_ty
163 = tcInstCall Rank2Origin actual_ty `thenNF_Tc` \ (inst_fn, lie1, body_ty) ->
164 tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie2) ->
165 returnTc (co_fn <.> mkCoercion inst_fn, lie1 `plusLIE` lie2)
167 -----------------------------------
170 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
171 = tcSub_fun exp_arg exp_res act_arg act_res
173 -----------------------------------
174 -- Type variable meets function: imitate
176 -- NB 1: we can't just unify the type variable with the type
177 -- because the type might not be a tau-type, and we aren't
178 -- allowed to instantiate an ordinary type variable with
181 -- NB 2: can we short-cut to an error case?
182 -- when the arg/res is not a tau-type?
183 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
185 -- is perfectly fine!
187 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
188 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
190 Just ty -> tc_sub exp_sty exp_ty ty ty
191 Nothing -> imitateFun tv exp_sty `thenNF_Tc` \ (act_arg, act_res) ->
192 tcSub_fun exp_arg exp_res act_arg act_res
194 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
195 = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
197 Just ty -> tc_sub ty ty act_sty act_ty
198 Nothing -> imitateFun tv act_sty `thenNF_Tc` \ (exp_arg, exp_res) ->
199 tcSub_fun exp_arg exp_res act_arg act_res
201 -----------------------------------
203 -- If none of the above match, we revert to the plain unifier
204 tc_sub exp_sty expected_ty act_sty actual_ty
205 = uTys exp_sty expected_ty act_sty actual_ty `thenTc_`
206 returnTc (idCoercion, emptyLIE)
209 %************************************************************************
211 \subsection{Functions}
213 %************************************************************************
216 tcSub_fun exp_arg exp_res act_arg act_res
217 = tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) ->
218 tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) ->
219 tcGetUnique `thenNF_Tc` \ uniq ->
221 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
222 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
223 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
224 arg_id = mkSysLocal SLIT("sub") uniq exp_arg
225 coercion | isIdCoercion co_fn_arg,
226 isIdCoercion co_fn_res = idCoercion
227 | otherwise = mkCoercion co_fn
229 co_fn e = DictLam [arg_id]
230 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
231 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
232 -- HsVar arg_id :: HsExpr exp_arg
233 -- co_fn_arg $it :: HsExpr act_arg
234 -- HsApp e $it :: HsExpr act_res
235 -- co_fn_res $it :: HsExpr exp_res
237 returnTc (coercion, lie1 `plusLIE` lie2)
239 imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType)
241 = ASSERT( not (isHoleTyVar tv) )
242 -- NB: tv is an *ordinary* tyvar and so are the new ones
244 -- Check that tv isn't a type-signature type variable
245 -- (This would be found later in checkSigTyVars, but
246 -- we get a better error message if we do it here.)
247 checkTcM (not (isSkolemTyVar tv))
248 (failWithTcM (unifyWithSigErr tv ty)) `thenTc_`
250 newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
251 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
252 putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_`
253 returnNF_Tc (arg,res)
257 %************************************************************************
259 \subsection{Generalisation}
261 %************************************************************************
264 tcGen :: TcSigmaType -- expected_ty
265 -> (TcPhiType -> TcM (result, LIE)) -- spec_ty
266 -> TcM (ExprCoFn, result, LIE)
267 -- The expression has type: spec_ty -> expected_ty
269 tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type
270 -- If not, the call is a no-op
271 = tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) ->
273 -- Type-check the arg and unify with poly type
274 thing_inside phi_ty `thenTc` \ (result, lie) ->
276 -- Check that the "forall_tvs" havn't been constrained
277 -- The interesting bit here is that we must include the free variables
278 -- of the expected_ty. Here's an example:
279 -- runST (newVar True)
280 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
281 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
282 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
283 -- So now s' isn't unconstrained because it's linked to a.
284 -- Conclusion: include the free vars of the expected_ty in the
285 -- list of "free vars" for the signature check.
287 tcExtendGlobalTyVars free_tvs $
288 tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $
290 newDicts SignatureOrigin theta `thenNF_Tc` \ dicts ->
291 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) ->
292 checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs ->
295 -- This HsLet binds any Insts which came out of the simplification.
296 -- It's a bit out of place here, but using AbsBind involves inventing
297 -- a couple of new names which seems worse.
298 dict_ids = map instToId dicts
299 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
301 returnTc (mkCoercion co_fn, result, free_lie)
303 free_tvs = tyVarsOfType expected_ty
304 sig_msg = ptext SLIT("When generalising the type of an expression")
309 %************************************************************************
311 \subsection{Coercion functions}
313 %************************************************************************
316 type Coercion a = Maybe (a -> a)
317 -- Nothing => identity fn
319 type ExprCoFn = Coercion TypecheckedHsExpr
320 type PatCoFn = Coercion TcPat
322 (<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition
323 Nothing <.> Nothing = Nothing
324 Nothing <.> Just f = Just f
325 Just f <.> Nothing = Just f
326 Just f1 <.> Just f2 = Just (f1 . f2)
328 (<$>) :: Coercion a -> a -> a
332 mkCoercion :: (a -> a) -> Coercion a
333 mkCoercion f = Just f
335 idCoercion :: Coercion a
338 isIdCoercion :: Coercion a -> Bool
339 isIdCoercion = isNothing
342 %************************************************************************
344 \subsection[Unify-exported]{Exported unification functions}
346 %************************************************************************
348 The exported functions are all defined as versions of some
349 non-exported generic functions.
351 Unify two @TauType@s. Dead straightforward.
354 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
355 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
356 = -- The unifier should only ever see tau-types
357 -- (no quantification whatsoever)
358 ASSERT2( isTauTy ty1, ppr ty1 )
359 ASSERT2( isTauTy ty2, ppr ty2 )
360 tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
364 @unifyTauTyList@ unifies corresponding elements of two lists of
365 @TauType@s. It uses @uTys@ to do the real work. The lists should be
366 of equal length. We charge down the list explicitly so that we can
367 complain if their lengths differ.
370 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
371 unifyTauTyLists [] [] = returnTc ()
372 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
373 unifyTauTyLists tys1 tys2
374 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
377 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
378 all together. It is used, for example, when typechecking explicit
379 lists, when all the elts should be of the same type.
382 unifyTauTyList :: [TcTauType] -> TcM ()
383 unifyTauTyList [] = returnTc ()
384 unifyTauTyList [ty] = returnTc ()
385 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
389 %************************************************************************
391 \subsection[Unify-uTys]{@uTys@: getting down to business}
393 %************************************************************************
395 @uTys@ is the heart of the unifier. Each arg happens twice, because
396 we want to report errors in terms of synomyms if poss. The first of
397 the pair is used in error messages only; it is always the same as the
398 second, except that if the first is a synonym then the second may be a
399 de-synonym'd version. This way we get better error messages.
401 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
404 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
405 -- ty1 is the *expected* type
407 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
408 -- ty2 is the *actual* type
411 -- Always expand synonyms (see notes at end)
412 -- (this also throws away FTVs)
413 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
414 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
416 -- Variables; go for uVar
417 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
418 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
419 -- "True" means args swapped
422 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
423 | n1 == n2 = uTys t1 t1 t2 t2
424 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
425 | c1 == c2 = unifyTauTyLists tys1 tys2
426 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
427 | tc1 == tc2 = unifyTauTyLists tys1 tys2
429 -- Functions; just check the two parts
430 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
431 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
433 -- Type constructors must match
434 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
435 | con1 == con2 && equalLength tys1 tys2
436 = unifyTauTyLists tys1 tys2
438 | con1 == openKindCon
439 -- When we are doing kind checking, we might match a kind '?'
440 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
441 -- (CCallable Int) and (CCallable Int#) are both OK
442 = unifyOpenTypeKind ps_ty2
444 -- Applications need a bit of care!
445 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
446 -- NB: we've already dealt with type variables and Notes,
447 -- so if one type is an App the other one jolly well better be too
448 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
449 = case tcSplitAppTy_maybe ty2 of
450 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
451 Nothing -> unifyMisMatch ps_ty1 ps_ty2
453 -- Now the same, but the other way round
454 -- Don't swap the types, because the error messages get worse
455 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
456 = case tcSplitAppTy_maybe ty1 of
457 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
458 Nothing -> unifyMisMatch ps_ty1 ps_ty2
460 -- Not expecting for-alls in unification
461 -- ... but the error message from the unifyMisMatch more informative
462 -- than a panic message!
464 -- Anything else fails
465 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
471 If you are tempted to make a short cut on synonyms, as in this
475 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
476 -- NO = if (con1 == con2) then
477 -- NO -- Good news! Same synonym constructors, so we can shortcut
478 -- NO -- by unifying their arguments and ignoring their expansions.
479 -- NO unifyTauTypeLists args1 args2
481 -- NO -- Never mind. Just expand them and try again
485 then THINK AGAIN. Here is the whole story, as detected and reported
486 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
488 Here's a test program that should detect the problem:
492 x = (1 :: Bogus Char) :: Bogus Bool
495 The problem with [the attempted shortcut code] is that
499 is not a sufficient condition to be able to use the shortcut!
500 You also need to know that the type synonym actually USES all
501 its arguments. For example, consider the following type synonym
502 which does not use all its arguments.
507 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
508 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
509 would fail, even though the expanded forms (both \tr{Int}) should
512 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
513 unnecessarily bind \tr{t} to \tr{Char}.
515 ... You could explicitly test for the problem synonyms and mark them
516 somehow as needing expansion, perhaps also issuing a warning to the
521 %************************************************************************
523 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
525 %************************************************************************
527 @uVar@ is called when at least one of the types being unified is a
528 variable. It does {\em not} assume that the variable is a fixed point
529 of the substitution; rather, notice that @uVar@ (defined below) nips
530 back into @uTys@ if it turns out that the variable is already bound.
533 uVar :: Bool -- False => tyvar is the "expected"
534 -- True => ty is the "expected" thing
536 -> TcTauType -> TcTauType -- printing and real versions
539 uVar swapped tv1 ps_ty2 ty2
540 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenNF_Tc_`
541 getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
543 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
544 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
545 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
547 -- Expand synonyms; ignore FTVs
548 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
549 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
552 -- The both-type-variable case
553 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
555 -- Same type variable => no-op
559 -- Distinct type variables
560 -- ASSERT maybe_ty1 /= Just
562 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
564 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
568 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
569 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
573 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
574 putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
579 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
580 -- Try to get rid of open type variables as soon as poss
582 nicer_to_update_tv2 = isUserTyVar tv1
583 -- Don't unify a signature type variable if poss
584 || isSystemName (varName tv2)
585 -- Try to update sys-y type variables in preference to sig-y ones
587 -- Second one isn't a type variable
588 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
589 = -- Check that tv1 isn't a type-signature type variable
590 checkTcM (not (isSkolemTyVar tv1))
591 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
593 -- Do the occurs check, and check that we are not
594 -- unifying a type variable with a polytype
595 -- Returns a zonked type ready for the update
596 checkValue tv1 ps_ty2 non_var_ty2 `thenTc` \ ty2 ->
598 -- Check that the kinds match
599 checkKinds swapped tv1 ty2 `thenTc_`
601 -- Perform the update
602 putTcTyVar tv1 ty2 `thenNF_Tc_`
607 checkKinds swapped tv1 ty2
608 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
609 -- ty2 has been zonked at this stage, which ensures that
610 -- its kind has as much boxity information visible as possible.
611 | tk2 `hasMoreBoxityInfo` tk1 = returnTc ()
614 -- Either the kinds aren't compatible
615 -- (can happen if we unify (a b) with (c d))
616 -- or we are unifying a lifted type variable with an
617 -- unlifted type: e.g. (id 3#) is illegal
618 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
622 (k1,k2) | swapped = (tk2,tk1)
623 | otherwise = (tk1,tk2)
629 checkValue tv1 ps_ty2 non_var_ty2
630 -- Do the occurs check, and check that we are not
631 -- unifying a type variable with a polytype
632 -- Return the type to update the type variable with, or fail
634 -- Basically we want to update tv1 := ps_ty2
635 -- because ps_ty2 has type-synonym info, which improves later error messages
640 -- f :: (A a -> a -> ()) -> ()
644 -- x = f (\ x p -> p x)
646 -- In the application (p x), we try to match "t" with "A t". If we go
647 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
648 -- an infinite loop later.
649 -- But we should not reject the program, because A t = ().
650 -- Rather, we should bind t to () (= non_var_ty2).
652 -- That's why we have this two-state occurs-check
653 = zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
654 case okToUnifyWith tv1 ps_ty2' of {
655 Nothing -> returnTc ps_ty2' ; -- Success
658 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
659 case okToUnifyWith tv1 non_var_ty2' of
660 Nothing -> -- This branch rarely succeeds, except in strange cases
661 -- like that in the example above
662 returnTc non_var_ty2'
664 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
667 data Problem = OccurCheck | NotMonoType
669 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
670 -- (okToUnifyWith tv ty) checks whether it's ok to unify
673 -- Just p => not ok, problem p
678 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
679 | otherwise = Nothing
680 ok (AppTy t1 t2) = ok t1 `and` ok t2
681 ok (FunTy t1 t2) = ok t1 `and` ok t2
682 ok (TyConApp _ ts) = oks ts
683 ok (ForAllTy _ _) = Just NotMonoType
684 ok (SourceTy st) = ok_st st
685 ok (NoteTy (FTVNote _) t) = ok t
686 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
687 -- Type variables may be free in t1 but not t2
688 -- A forall may be in t2 but not t1
690 oks ts = foldr (and . ok) Nothing ts
692 ok_st (ClassP _ ts) = oks ts
693 ok_st (IParam _ t) = ok t
694 ok_st (NType _ ts) = oks ts
697 Just p `and` m = Just p
700 %************************************************************************
702 \subsection[Unify-fun]{@unifyFunTy@}
704 %************************************************************************
706 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
707 creation of type variables.
709 * subFunTy is used when we might be faced with a "hole" type variable,
710 in which case we should create two new holes.
712 * unifyFunTy is used when we expect to encounter only "ordinary"
713 type variables, so we should create new ordinary type variables
716 subFunTy :: TcSigmaType -- Fail if ty isn't a function type
717 -> TcM (TcType, TcType) -- otherwise return arg and result types
718 subFunTy ty@(TyVarTy tyvar)
720 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
722 Just ty -> subFunTy ty
723 Nothing | isHoleTyVar tyvar
724 -> newHoleTyVarTy `thenNF_Tc` \ arg ->
725 newHoleTyVarTy `thenNF_Tc` \ res ->
726 putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_`
729 -> unify_fun_ty_help ty
732 = case tcSplitFunTy_maybe ty of
733 Just arg_and_res -> returnTc arg_and_res
734 Nothing -> unify_fun_ty_help ty
737 unifyFunTy :: TcPhiType -- Fail if ty isn't a function type
738 -> TcM (TcType, TcType) -- otherwise return arg and result types
740 unifyFunTy ty@(TyVarTy tyvar)
741 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
743 Just ty' -> unifyFunTy ty'
744 Nothing -> unify_fun_ty_help ty
747 = case tcSplitFunTy_maybe ty of
748 Just arg_and_res -> returnTc arg_and_res
749 Nothing -> unify_fun_ty_help ty
751 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
752 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
753 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
754 unifyTauTy ty (mkFunTy arg res) `thenTc_`
759 unifyListTy :: TcType -- expected list type
760 -> TcM TcType -- list element type
762 unifyListTy ty@(TyVarTy tyvar)
763 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
765 Just ty' -> unifyListTy ty'
766 other -> unify_list_ty_help ty
769 = case tcSplitTyConApp_maybe ty of
770 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
771 other -> unify_list_ty_help ty
773 unify_list_ty_help ty -- Revert to ordinary unification
774 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
775 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
778 -- variant for parallel arrays
780 unifyPArrTy :: TcType -- expected list type
781 -> TcM TcType -- list element type
783 unifyPArrTy ty@(TyVarTy tyvar)
784 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
786 Just ty' -> unifyPArrTy ty'
787 _ -> unify_parr_ty_help ty
789 = case tcSplitTyConApp_maybe ty of
790 Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnTc arg_ty
791 _ -> unify_parr_ty_help ty
793 unify_parr_ty_help ty -- Revert to ordinary unification
794 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
795 unifyTauTy ty (mkPArrTy elt_ty) `thenTc_`
800 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
801 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
802 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
804 Just ty' -> unifyTupleTy boxity arity ty'
805 other -> unify_tuple_ty_help boxity arity ty
807 unifyTupleTy boxity arity ty
808 = case tcSplitTyConApp_maybe ty of
809 Just (tycon, arg_tys)
811 && tyConArity tycon == arity
812 && tupleTyConBoxity tycon == boxity
814 other -> unify_tuple_ty_help boxity arity ty
816 unify_tuple_ty_help boxity arity ty
817 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
818 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
821 kind | isBoxed boxity = liftedTypeKind
822 | otherwise = openTypeKind
826 %************************************************************************
828 \subsection{Kind unification}
830 %************************************************************************
833 unifyKind :: TcKind -- Expected
837 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
840 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
841 unifyKinds [] [] = returnTc ()
842 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
844 unifyKinds _ _ = panic "unifyKinds: length mis-match"
848 unifyOpenTypeKind :: TcKind -> TcM ()
849 -- Ensures that the argument kind is of the form (Type bx)
850 -- for some boxity bx
852 unifyOpenTypeKind ty@(TyVarTy tyvar)
853 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
855 Just ty' -> unifyOpenTypeKind ty'
856 other -> unify_open_kind_help ty
859 | isTypeKind ty = returnTc ()
860 | otherwise = unify_open_kind_help ty
862 unify_open_kind_help ty -- Revert to ordinary unification
863 = newBoxityVar `thenNF_Tc` \ boxity ->
864 unifyKind ty (mkTyConApp typeCon [boxity])
868 %************************************************************************
870 \subsection[Unify-context]{Errors and contexts}
872 %************************************************************************
878 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
879 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
880 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
881 returnNF_Tc (err ty1' ty2')
886 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
887 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
890 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
892 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
893 -- tv1 is zonked already
894 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
895 returnNF_Tc (err ty2')
897 err ty2 = (env2, ptext SLIT("When matching types") <+>
898 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
900 (pp_expected, pp_actual) | swapped = (pp2, pp1)
901 | otherwise = (pp1, pp2)
902 (env1, tv1') = tidyOpenTyVar tidy_env tv1
903 (env2, ty2') = tidyOpenType env1 ty2
907 unifyMisMatch ty1 ty2
908 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
909 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
911 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
912 msg = hang (ptext SLIT("Couldn't match"))
913 4 (sep [quotes (ppr tidy_ty1),
914 ptext SLIT("against"),
915 quotes (ppr tidy_ty2)])
917 failWithTcM (env, msg)
919 unifyWithSigErr tyvar ty
920 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
921 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
923 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
924 (env2, tidy_ty) = tidyOpenType env1 ty
926 unifyCheck problem tyvar ty
928 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
930 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
931 (env2, tidy_ty) = tidyOpenType env1 ty
933 msg = case problem of
934 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
935 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
940 %************************************************************************
942 \subsection{Checking signature type variables}
944 %************************************************************************
946 @checkSigTyVars@ is used after the type in a type signature has been unified with
947 the actual type found. It then checks that the type variables of the type signature
949 (a) Still all type variables
950 eg matching signature [a] against inferred type [(p,q)]
951 [then a will be unified to a non-type variable]
953 (b) Still all distinct
954 eg matching signature [(a,b)] against inferred type [(p,p)]
955 [then a and b will be unified together]
957 (c) Not mentioned in the environment
958 eg the signature for f in this:
964 Here, f is forced to be monorphic by the free occurence of x.
966 (d) Not (unified with another type variable that is) in scope.
967 eg f x :: (r->r) = (\y->y) :: forall a. a->r
968 when checking the expression type signature, we find that
969 even though there is nothing in scope whose type mentions r,
970 nevertheless the type signature for the expression isn't right.
972 Another example is in a class or instance declaration:
974 op :: forall b. a -> b
976 Here, b gets unified with a
978 Before doing this, the substitution is applied to the signature type variable.
980 We used to have the notion of a "DontBind" type variable, which would
981 only be bound to itself or nothing. Then points (a) and (b) were
982 self-checking. But it gave rise to bogus consequential error messages.
985 f = (*) -- Monomorphic
990 Here, we get a complaint when checking the type signature for g,
991 that g isn't polymorphic enough; but then we get another one when
992 dealing with the (Num x) context arising from f's definition;
993 we try to unify x with Int (to default it), but find that x has already
994 been unified with the DontBind variable "a" from g's signature.
995 This is really a problem with side-effecting unification; we'd like to
996 undo g's effects when its type signature fails, but unification is done
997 by side effect, so we can't (easily).
999 So we revert to ordinary type variables for signatures, and try to
1000 give a helpful message in checkSigTyVars.
1003 checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
1004 -> TcTyVarSet -- Tyvars that are free in the type signature
1005 -- Not necessarily zonked
1006 -- These should *already* be in the free-in-env set,
1007 -- and are used here only to improve the error message
1008 -> TcM [TcTyVar] -- Zonked signature type variables
1010 checkSigTyVars [] free = returnTc []
1011 checkSigTyVars sig_tyvars free_tyvars
1012 = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
1013 tcGetGlobalTyVars `thenNF_Tc` \ globals ->
1015 checkTcM (allDistinctTyVars sig_tys globals)
1016 (complain sig_tys globals) `thenTc_`
1018 returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
1021 complain sig_tys globals
1022 = -- "check" checks each sig tyvar in turn
1024 (env2, emptyVarEnv, [])
1025 (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) ->
1027 failWithTcM (env3, main_msg $$ vcat msgs)
1029 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
1030 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1032 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1034 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1035 -- sig_tyvar is from the signature;
1036 -- ty is what you get if you zonk sig_tyvar and then tidy it
1038 -- acc maps a zonked type variable back to a signature type variable
1039 = case tcGetTyVar_maybe ty of {
1040 Nothing -> -- Error (a)!
1041 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1045 case lookupVarEnv acc tv of {
1046 Just sig_tyvar' -> -- Error (b)!
1047 returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1049 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1053 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1054 -- The least comprehensible, so put it last
1056 -- a) get the local TcIds and TyVars from the environment,
1057 -- and pass them to find_globals (they might have tv free)
1058 -- b) similarly, find any free_tyvars that mention tv
1059 then tcGetEnv `thenNF_Tc` \ ve ->
1060 find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) ->
1061 find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) ->
1062 returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
1065 returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1068 -----------------------
1069 -- find_globals looks at the value environment and finds values
1070 -- whose types mention the offending type variable. It has to be
1071 -- careful to zonk the Id's type first, so it has to be in the monad.
1072 -- We must be careful to pass it a zonked type variable, too.
1077 -> NF_TcM (TidyEnv, [SDoc])
1079 find_globals tv tidy_env things
1080 = go tidy_env [] things
1082 go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
1083 go tidy_env acc (thing : things)
1084 = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
1086 Just d -> go tidy_env1 (d:acc) things
1087 Nothing -> go tidy_env1 acc things
1089 ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
1091 -----------------------
1092 find_thing ignore_it tidy_env (ATcId id)
1093 = zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
1094 if ignore_it id_ty then
1095 returnNF_Tc (tidy_env, Nothing)
1097 (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
1098 msg = sep [ppr id <+> dcolon <+> ppr tidy_ty,
1099 nest 2 (parens (ptext SLIT("bound at") <+>
1100 ppr (getSrcLoc id)))]
1102 returnNF_Tc (tidy_env', Just msg)
1104 find_thing ignore_it tidy_env (ATyVar tv)
1105 = zonkTcTyVar tv `thenNF_Tc` \ tv_ty ->
1106 if ignore_it tv_ty then
1107 returnNF_Tc (tidy_env, Nothing)
1109 (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv
1110 (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty
1111 msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
1113 eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
1114 | otherwise = equals <+> ppr tv_ty
1115 -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
1117 bound_at = tyVarBindingInfo tv
1119 returnNF_Tc (tidy_env2, Just msg)
1121 -----------------------
1122 find_frees tv tidy_env acc []
1123 = returnNF_Tc (tidy_env, acc)
1124 find_frees tv tidy_env acc (ftv:ftvs)
1125 = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
1126 if tv `elemVarSet` tyVarsOfType ty then
1128 (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
1130 find_frees tv tidy_env' (ftv':acc) ftvs
1132 find_frees tv tidy_env acc ftvs
1135 escape_msg sig_tv tv globs frees
1136 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1137 if not (null globs) then
1138 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1139 nest 2 (vcat globs)]
1140 else if not (null frees) then
1141 vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
1142 nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
1145 empty -- Sigh. It's really hard to give a good error message
1146 -- all the time. One bad case is an existential pattern match
1148 is_are | isSingleton frees = ptext SLIT("is")
1149 | otherwise = ptext SLIT("are")
1150 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1151 | otherwise = ptext SLIT("It")
1153 vcat_first :: Int -> [SDoc] -> SDoc
1154 vcat_first n [] = empty
1155 vcat_first 0 (x:xs) = text "...others omitted..."
1156 vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
1159 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1160 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1163 These two context are used with checkSigTyVars
1166 sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType
1167 -> TidyEnv -> NF_TcM (TidyEnv, Message)
1168 sigCtxt sig_tyvars sig_theta sig_tau tidy_env
1169 = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
1171 (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars
1172 (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
1173 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1174 msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
1175 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1178 returnNF_Tc (env3, msg)
1180 sigPatCtxt bound_tvs bound_ids tidy_env
1181 = returnNF_Tc (env1,
1182 sep [ptext SLIT("When checking a pattern that binds"),
1183 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
1185 show_ids = filter is_interesting bound_ids
1186 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
1188 (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1189 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1190 -- Don't zonk the types so we get the separate, un-unified versions