2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubOff, tcSubExp, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyKind, unifyKinds, unifyFunKind,
16 --------------------------------
18 Expected(..), newHole, readExpectedType,
19 zapExpectedType, zapExpectedTo, zapExpectedBranches,
20 subFunTys, unifyFunTy,
21 zapToListTy, unifyListTy,
22 zapToPArrTy, unifyPArrTy,
23 zapToTupleTy, unifyTupleTy
27 #include "HsVersions.h"
30 import HsSyn ( HsExpr(..) )
31 import TcHsSyn ( mkHsLet, mkHsDictLam,
32 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
33 import TypeRep ( Type(..), PredType(..), TyNote(..), openKindCon, isSuperKind )
35 import TcRnMonad -- TcType, amongst others
36 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
37 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
38 isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
39 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
40 tcGetTyVar_maybe, tcGetTyVar,
41 mkFunTy, tyVarsOfType, mkPhiTy,
42 typeKind, tcSplitFunTy_maybe, mkForAllTys,
43 isSkolemTyVar, isUserTyVar,
44 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
45 eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
46 hasMoreBoxityInfo, allDistinctTyVars, pprType, pprKind )
47 import Inst ( newDicts, instToId, tcInstCall )
48 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
49 newTyVarTy, newTyVarTys, newOpenTypeKind,
50 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV )
51 import TcSimplify ( tcSimplifyCheck )
52 import TysWiredIn ( listTyCon, parrTyCon, tupleTyCon )
53 import TcEnv ( tcGetGlobalTyVars, findGlobals )
54 import TyCon ( TyCon, tyConArity, isTupleTyCon, tupleTyConBoxity )
55 import Id ( Id, mkSysLocal )
56 import Var ( Var, varName, tyVarKind )
57 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
59 import Name ( isSystemName )
60 import ErrUtils ( Message )
61 import SrcLoc ( noLoc )
62 import BasicTypes ( Boxity, Arity, isBoxed )
63 import Util ( equalLength, lengthExceeds, notNull )
69 * A hole is always filled in with an ordinary type, not another hole.
71 %************************************************************************
73 \subsection{'hole' type variables}
75 %************************************************************************
78 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
79 | Check ty -- The type to check during type checking
81 newHole :: TcM (TcRef ty)
82 newHole = newMutVar (error "Empty hole in typechecker")
84 readExpectedType :: Expected ty -> TcM ty
85 readExpectedType (Infer hole) = readMutVar hole
86 readExpectedType (Check ty) = returnM ty
88 zapExpectedType :: Expected TcType -> TcM TcTauType
89 -- In the inference case, ensure we have a monotype
90 zapExpectedType (Infer hole)
91 = do { ty <- newTyVarTy openTypeKind ;
95 zapExpectedType (Check ty) = return ty
97 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
98 zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
99 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
101 zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
102 -- Zap the expected type to a monotype if there is more than one branch
103 zapExpectedBranches branches exp_ty
104 | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' ->
105 return (Check exp_ty')
106 | otherwise = returnM exp_ty
108 instance Outputable ty => Outputable (Expected ty) where
109 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
110 ppr (Infer hole) = ptext SLIT("Inferring type")
114 %************************************************************************
116 \subsection[Unify-fun]{@unifyFunTy@}
118 %************************************************************************
120 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
121 creation of type variables.
123 * subFunTy is used when we might be faced with a "hole" type variable,
124 in which case we should create two new holes.
126 * unifyFunTy is used when we expect to encounter only "ordinary"
127 type variables, so we should create new ordinary type variables
131 -> Expected TcRhoType -- Fail if ty isn't a function type
132 -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a)
135 subFunTys pats (Infer hole) thing_inside
136 = -- This is the interesting case
137 mapM new_pat_hole pats `thenM` \ pats_w_holes ->
138 newHole `thenM` \ res_hole ->
141 thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer ->
143 -- Extract the answers
144 mapM read_pat_hole pats_w_holes `thenM` \ arg_tys ->
145 readMutVar res_hole `thenM` \ res_ty ->
147 -- Write the answer into the incoming hole
148 writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_`
150 -- And return the answer
153 new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole)
154 read_pat_hole (pat, Infer hole) = readMutVar hole
156 subFunTys pats (Check ty) thing_inside
157 = go pats ty `thenM` \ (pats_w_tys, res_ty) ->
158 thing_inside pats_w_tys res_ty
160 go [] ty = return ([], Check ty)
161 go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) ->
162 go pats res `thenM` \ (pats_w_tys, final_res) ->
163 return ((pat, Check arg) : pats_w_tys, final_res)
165 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
166 -> TcM (TcType, TcType) -- otherwise return arg and result types
168 unifyFunTy ty@(TyVarTy tyvar)
169 = getTcTyVar tyvar `thenM` \ maybe_ty ->
171 Just ty' -> unifyFunTy ty'
172 Nothing -> unify_fun_ty_help ty
175 = case tcSplitFunTy_maybe ty of
176 Just arg_and_res -> returnM arg_and_res
177 Nothing -> unify_fun_ty_help ty
179 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
180 = newTyVarTy openTypeKind `thenM` \ arg ->
181 newTyVarTy openTypeKind `thenM` \ res ->
182 unifyTauTy ty (mkFunTy arg res) `thenM_`
187 ----------------------
188 zapToListTy, zapToPArrTy :: Expected TcType -- expected list type
189 -> TcM TcType -- list element type
190 unifyListTy, unifyPArrTy :: TcType -> TcM TcType
191 zapToListTy = zapToXTy listTyCon
192 unifyListTy = unifyXTy listTyCon
193 zapToPArrTy = zapToXTy parrTyCon
194 unifyPArrTy = unifyXTy parrTyCon
196 ----------------------
197 zapToXTy :: TyCon -- T :: *->*
198 -> Expected TcType -- Expected type (T a)
199 -> TcM TcType -- Element type, a
201 zapToXTy tc (Check ty) = unifyXTy tc ty
202 zapToXTy tc (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
203 writeMutVar hole (mkTyConApp tc [elt_ty]) ;
206 ----------------------
207 unifyXTy :: TyCon -> TcType -> TcM TcType
208 unifyXTy tc ty@(TyVarTy tyvar)
209 = getTcTyVar tyvar `thenM` \ maybe_ty ->
211 Just ty' -> unifyXTy tc ty'
212 other -> unify_x_ty_help tc ty
215 = case tcSplitTyConApp_maybe ty of
216 Just (tycon, [arg_ty]) | tycon == tc -> returnM arg_ty
217 other -> unify_x_ty_help tc ty
219 unify_x_ty_help tc ty -- Revert to ordinary unification
220 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
221 unifyTauTy ty (mkTyConApp tc [elt_ty]) `thenM_`
226 ----------------------
227 zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
228 zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
229 zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
230 writeMutVar hole tup_ty ;
233 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
234 = getTcTyVar tyvar `thenM` \ maybe_ty ->
236 Just ty' -> unifyTupleTy boxity arity ty'
237 other -> unify_tuple_ty_help boxity arity ty
239 unifyTupleTy boxity arity ty
240 = case tcSplitTyConApp_maybe ty of
241 Just (tycon, arg_tys)
243 && tyConArity tycon == arity
244 && tupleTyConBoxity tycon == boxity
246 other -> unify_tuple_ty_help boxity arity ty
248 unify_tuple_ty_help boxity arity ty
249 = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
250 unifyTauTy ty tup_ty `thenM_`
253 new_tuple_ty boxity arity
254 = newTyVarTys arity kind `thenM` \ arg_tys ->
255 return (mkTyConApp tup_tc arg_tys, arg_tys)
257 tup_tc = tupleTyCon boxity arity
258 kind | isBoxed boxity = liftedTypeKind
259 | otherwise = openTypeKind
263 %************************************************************************
265 \subsection{Subsumption}
267 %************************************************************************
269 All the tcSub calls have the form
271 tcSub expected_ty offered_ty
273 offered_ty <= expected_ty
275 That is, that a value of type offered_ty is acceptable in
276 a place expecting a value of type expected_ty.
278 It returns a coercion function
279 co_fn :: offered_ty -> expected_ty
280 which takes an HsExpr of type offered_ty into one of type
284 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
285 tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
288 These two check for holes
291 tcSubExp expected_ty offered_ty
292 = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_`
293 checkHole expected_ty offered_ty tcSub
295 tcSubOff expected_ty offered_ty
296 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
298 -- checkHole looks for a hole in its first arg;
299 -- If so, and it is uninstantiated, it fills in the hole
300 -- with its second arg
301 -- Otherwise it calls thing_inside, passing the two args, looking
302 -- through any instantiated hole
304 checkHole (Infer hole) other_ty thing_inside
305 = do { writeMutVar hole other_ty; return idCoercion }
307 checkHole (Check ty) other_ty thing_inside
308 = thing_inside ty other_ty
311 No holes expected now. Add some error-check context info.
314 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
315 tcSub expected_ty actual_ty
316 = traceTc (text "tcSub" <+> details) `thenM_`
317 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
318 (tc_sub expected_ty expected_ty actual_ty actual_ty)
320 details = vcat [text "Expected:" <+> ppr expected_ty,
321 text "Actual: " <+> ppr actual_ty]
324 tc_sub carries the types before and after expanding type synonyms
327 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
328 -> TcSigmaType -- ..and after
329 -> TcSigmaType -- actual_ty, before
330 -> TcSigmaType -- ..and after
333 -----------------------------------
335 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
336 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
338 -----------------------------------
339 -- Generalisation case
340 -- actual_ty: d:Eq b => b->b
341 -- expected_ty: forall a. Ord a => a->a
342 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
344 -- It is essential to do this *before* the specialisation case
345 -- Example: f :: (Eq a => a->a) -> ...
346 -- g :: Ord b => b->b
349 tc_sub exp_sty expected_ty act_sty actual_ty
350 | isSigmaTy expected_ty
351 = tcGen expected_ty (tyVarsOfType actual_ty) (
352 -- It's really important to check for escape wrt the free vars of
353 -- both expected_ty *and* actual_ty
354 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
355 ) `thenM` \ (gen_fn, co_fn) ->
356 returnM (gen_fn <.> co_fn)
358 -----------------------------------
359 -- Specialisation case:
360 -- actual_ty: forall a. Ord a => a->a
361 -- expected_ty: Int -> Int
362 -- co_fn e = e Int dOrdInt
364 tc_sub exp_sty expected_ty act_sty actual_ty
365 | isSigmaTy actual_ty
366 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
367 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
368 returnM (co_fn <.> inst_fn)
370 -----------------------------------
373 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
374 = tcSub_fun exp_arg exp_res act_arg act_res
376 -----------------------------------
377 -- Type variable meets function: imitate
379 -- NB 1: we can't just unify the type variable with the type
380 -- because the type might not be a tau-type, and we aren't
381 -- allowed to instantiate an ordinary type variable with
384 -- NB 2: can we short-cut to an error case?
385 -- when the arg/res is not a tau-type?
386 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
388 -- is perfectly fine, because we can instantiat f's type to a monotype
390 -- However, we get can get jolly unhelpful error messages.
391 -- e.g. foo = id runST
393 -- Inferred type is less polymorphic than expected
394 -- Quantified type variable `s' escapes
395 -- Expected type: ST s a -> t
396 -- Inferred type: (forall s1. ST s1 a) -> a
397 -- In the first argument of `id', namely `runST'
398 -- In a right-hand side of function `foo': id runST
400 -- I'm not quite sure what to do about this!
402 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
403 = getTcTyVar tv `thenM` \ maybe_ty ->
405 Just ty -> tc_sub exp_sty exp_ty ty ty
406 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
407 tcSub_fun exp_arg exp_res act_arg act_res
409 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
410 = getTcTyVar tv `thenM` \ maybe_ty ->
412 Just ty -> tc_sub ty ty act_sty act_ty
413 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
414 tcSub_fun exp_arg exp_res act_arg act_res
416 -----------------------------------
418 -- If none of the above match, we revert to the plain unifier
419 tc_sub exp_sty expected_ty act_sty actual_ty
420 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
424 %************************************************************************
426 \subsection{Functions}
428 %************************************************************************
431 tcSub_fun exp_arg exp_res act_arg act_res
432 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
433 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
434 newUnique `thenM` \ uniq ->
436 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
437 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
438 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
439 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
440 coercion | isIdCoercion co_fn_arg,
441 isIdCoercion co_fn_res = idCoercion
442 | otherwise = mkCoercion co_fn
444 co_fn e = DictLam [arg_id]
445 (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
446 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
447 -- HsVar arg_id :: HsExpr exp_arg
448 -- co_fn_arg $it :: HsExpr act_arg
449 -- HsApp e $it :: HsExpr act_res
450 -- co_fn_res $it :: HsExpr exp_res
454 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
456 = -- NB: tv is an *ordinary* tyvar and so are the new ones
458 -- Check that tv isn't a type-signature type variable
459 -- (This would be found later in checkSigTyVars, but
460 -- we get a better error message if we do it here.)
461 checkM (not (isSkolemTyVar tv))
462 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
464 newTyVarTy openTypeKind `thenM` \ arg ->
465 newTyVarTy openTypeKind `thenM` \ res ->
466 putTcTyVar tv (mkFunTy arg res) `thenM_`
471 %************************************************************************
473 \subsection{Generalisation}
475 %************************************************************************
478 tcGen :: TcSigmaType -- expected_ty
479 -> TcTyVarSet -- Extra tyvars that the universally
480 -- quantified tyvars of expected_ty
481 -- must not be unified
482 -> (TcRhoType -> TcM result) -- spec_ty
483 -> TcM (ExprCoFn, result)
484 -- The expression has type: spec_ty -> expected_ty
486 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
487 -- If not, the call is a no-op
488 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
490 -- Type-check the arg and unify with poly type
491 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
493 -- Check that the "forall_tvs" havn't been constrained
494 -- The interesting bit here is that we must include the free variables
495 -- of the expected_ty. Here's an example:
496 -- runST (newVar True)
497 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
498 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
499 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
500 -- So now s' isn't unconstrained because it's linked to a.
501 -- Conclusion: include the free vars of the expected_ty in the
502 -- list of "free vars" for the signature check.
504 newDicts SignatureOrigin theta `thenM` \ dicts ->
505 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
508 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
509 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
510 text "expected_ty" <+> ppr expected_ty,
511 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
512 text "free_tvs" <+> ppr free_tvs,
513 text "forall_tys" <+> ppr forall_tys]) `thenM_`
516 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
518 traceTc (text "tcGen:done") `thenM_`
521 -- This HsLet binds any Insts which came out of the simplification.
522 -- It's a bit out of place here, but using AbsBind involves inventing
523 -- a couple of new names which seems worse.
524 dict_ids = map instToId dicts
525 co_fn e = TyLam zonked_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
527 returnM (mkCoercion co_fn, result)
529 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
530 sig_msg = ptext SLIT("expected type of an expression")
535 %************************************************************************
537 \subsection[Unify-exported]{Exported unification functions}
539 %************************************************************************
541 The exported functions are all defined as versions of some
542 non-exported generic functions.
544 Unify two @TauType@s. Dead straightforward.
547 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
548 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
549 = -- The unifier should only ever see tau-types
550 -- (no quantification whatsoever)
551 ASSERT2( isTauTy ty1, ppr ty1 )
552 ASSERT2( isTauTy ty2, ppr ty2 )
553 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
557 @unifyTauTyList@ unifies corresponding elements of two lists of
558 @TauType@s. It uses @uTys@ to do the real work. The lists should be
559 of equal length. We charge down the list explicitly so that we can
560 complain if their lengths differ.
563 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
564 unifyTauTyLists [] [] = returnM ()
565 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
566 unifyTauTyLists tys1 tys2
567 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
570 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
571 all together. It is used, for example, when typechecking explicit
572 lists, when all the elts should be of the same type.
575 unifyTauTyList :: [TcTauType] -> TcM ()
576 unifyTauTyList [] = returnM ()
577 unifyTauTyList [ty] = returnM ()
578 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
582 %************************************************************************
584 \subsection[Unify-uTys]{@uTys@: getting down to business}
586 %************************************************************************
588 @uTys@ is the heart of the unifier. Each arg happens twice, because
589 we want to report errors in terms of synomyms if poss. The first of
590 the pair is used in error messages only; it is always the same as the
591 second, except that if the first is a synonym then the second may be a
592 de-synonym'd version. This way we get better error messages.
594 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
597 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
598 -- ty1 is the *expected* type
600 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
601 -- ty2 is the *actual* type
604 -- Always expand synonyms (see notes at end)
605 -- (this also throws away FTVs)
606 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
607 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
609 -- Variables; go for uVar
610 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
611 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
612 -- "True" means args swapped
615 uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
616 | n1 == n2 = uTys t1 t1 t2 t2
617 uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2))
618 | c1 == c2 = unifyTauTyLists tys1 tys2
620 -- Functions; just check the two parts
621 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
622 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
624 -- NewType constructors must match
625 uTys _ (NewTcApp tc1 tys1) _ (NewTcApp tc2 tys2)
626 | tc1 == tc2 = unifyTauTyLists tys1 tys2
628 -- Ordinary type constructors must match
629 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
630 | con1 == con2 && equalLength tys1 tys2
631 = unifyTauTyLists tys1 tys2
633 | con1 == openKindCon
634 -- When we are doing kind checking, we might match a kind '?'
635 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
636 -- (CCallable Int) and (CCallable Int#) are both OK
637 = unifyTypeKind ps_ty2
639 -- Applications need a bit of care!
640 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
641 -- NB: we've already dealt with type variables and Notes,
642 -- so if one type is an App the other one jolly well better be too
643 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
644 = case tcSplitAppTy_maybe ty2 of
645 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
646 Nothing -> unifyMisMatch ps_ty1 ps_ty2
648 -- Now the same, but the other way round
649 -- Don't swap the types, because the error messages get worse
650 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
651 = case tcSplitAppTy_maybe ty1 of
652 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
653 Nothing -> unifyMisMatch ps_ty1 ps_ty2
655 -- Not expecting for-alls in unification
656 -- ... but the error message from the unifyMisMatch more informative
657 -- than a panic message!
659 -- Anything else fails
660 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
666 If you are tempted to make a short cut on synonyms, as in this
670 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
671 -- NO = if (con1 == con2) then
672 -- NO -- Good news! Same synonym constructors, so we can shortcut
673 -- NO -- by unifying their arguments and ignoring their expansions.
674 -- NO unifyTauTypeLists args1 args2
676 -- NO -- Never mind. Just expand them and try again
680 then THINK AGAIN. Here is the whole story, as detected and reported
681 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
683 Here's a test program that should detect the problem:
687 x = (1 :: Bogus Char) :: Bogus Bool
690 The problem with [the attempted shortcut code] is that
694 is not a sufficient condition to be able to use the shortcut!
695 You also need to know that the type synonym actually USES all
696 its arguments. For example, consider the following type synonym
697 which does not use all its arguments.
702 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
703 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
704 would fail, even though the expanded forms (both \tr{Int}) should
707 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
708 unnecessarily bind \tr{t} to \tr{Char}.
710 ... You could explicitly test for the problem synonyms and mark them
711 somehow as needing expansion, perhaps also issuing a warning to the
716 %************************************************************************
718 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
720 %************************************************************************
722 @uVar@ is called when at least one of the types being unified is a
723 variable. It does {\em not} assume that the variable is a fixed point
724 of the substitution; rather, notice that @uVar@ (defined below) nips
725 back into @uTys@ if it turns out that the variable is already bound.
728 uVar :: Bool -- False => tyvar is the "expected"
729 -- True => ty is the "expected" thing
731 -> TcTauType -> TcTauType -- printing and real versions
734 uVar swapped tv1 ps_ty2 ty2
735 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
736 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
738 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
739 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
740 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
742 -- Expand synonyms; ignore FTVs
743 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
744 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
747 -- The both-type-variable case
748 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
750 -- Same type variable => no-op
754 -- Distinct type variables
755 -- ASSERT maybe_ty1 /= Just
757 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
759 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
763 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
764 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
768 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
769 putTcTyVar tv1 ps_ty2 `thenM_`
774 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
775 -- Try to get rid of open type variables as soon as poss
777 nicer_to_update_tv2 = isUserTyVar tv1
778 -- Don't unify a signature type variable if poss
779 || isSystemName (varName tv2)
780 -- Try to update sys-y type variables in preference to sig-y ones
782 -- Second one isn't a type variable
783 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
784 = -- Check that tv1 isn't a type-signature type variable
785 checkM (not (isSkolemTyVar tv1))
786 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
788 -- Do the occurs check, and check that we are not
789 -- unifying a type variable with a polytype
790 -- Returns a zonked type ready for the update
791 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
793 -- Check that the kinds match
794 checkKinds swapped tv1 ty2 `thenM_`
796 -- Perform the update
797 putTcTyVar tv1 ty2 `thenM_`
802 checkKinds swapped tv1 ty2
803 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
804 -- ty2 has been zonked at this stage, which ensures that
805 -- its kind has as much boxity information visible as possible.
806 | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
809 -- Either the kinds aren't compatible
810 -- (can happen if we unify (a b) with (c d))
811 -- or we are unifying a lifted type variable with an
812 -- unlifted type: e.g. (id 3#) is illegal
813 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
817 (k1,k2) | swapped = (tk2,tk1)
818 | otherwise = (tk1,tk2)
824 checkValue tv1 ps_ty2 non_var_ty2
825 -- Do the occurs check, and check that we are not
826 -- unifying a type variable with a polytype
827 -- Return the type to update the type variable with, or fail
829 -- Basically we want to update tv1 := ps_ty2
830 -- because ps_ty2 has type-synonym info, which improves later error messages
835 -- f :: (A a -> a -> ()) -> ()
839 -- x = f (\ x p -> p x)
841 -- In the application (p x), we try to match "t" with "A t". If we go
842 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
843 -- an infinite loop later.
844 -- But we should not reject the program, because A t = ().
845 -- Rather, we should bind t to () (= non_var_ty2).
847 -- That's why we have this two-state occurs-check
848 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
849 case okToUnifyWith tv1 ps_ty2' of {
850 Nothing -> returnM ps_ty2' ; -- Success
853 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
854 case okToUnifyWith tv1 non_var_ty2' of
855 Nothing -> -- This branch rarely succeeds, except in strange cases
856 -- like that in the example above
859 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
862 data Problem = OccurCheck | NotMonoType
864 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
865 -- (okToUnifyWith tv ty) checks whether it's ok to unify
868 -- Just p => not ok, problem p
873 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
874 | otherwise = Nothing
875 ok (AppTy t1 t2) = ok t1 `and` ok t2
876 ok (FunTy t1 t2) = ok t1 `and` ok t2
877 ok (TyConApp _ ts) = oks ts
878 ok (NewTcApp _ ts) = oks ts
879 ok (ForAllTy _ _) = Just NotMonoType
880 ok (PredTy st) = ok_st st
881 ok (NoteTy (FTVNote _) t) = ok t
882 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
883 -- Type variables may be free in t1 but not t2
884 -- A forall may be in t2 but not t1
886 oks ts = foldr (and . ok) Nothing ts
888 ok_st (ClassP _ ts) = oks ts
889 ok_st (IParam _ t) = ok t
892 Just p `and` m = Just p
895 %************************************************************************
897 \subsection{Kind unification}
899 %************************************************************************
902 unifyKind :: TcKind -- Expected
905 unifyKind k1 k2 = uTys k1 k1 k2 k2
907 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
908 unifyKinds [] [] = returnM ()
909 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
911 unifyKinds _ _ = panic "unifyKinds: length mis-match"
915 unifyTypeKind :: TcKind -> TcM ()
916 -- Ensures that the argument kind is a liftedTypeKind or unliftedTypeKind
917 -- If it's a kind variable, make it (Type bx), for a fresh boxity variable bx
919 unifyTypeKind ty@(TyVarTy tyvar)
920 = getTcTyVar tyvar `thenM` \ maybe_ty ->
922 Just ty' -> unifyTypeKind ty'
923 Nothing -> newOpenTypeKind `thenM` \ kind ->
924 putTcTyVar tyvar kind `thenM_`
928 | isTypeKind ty = returnM ()
929 | otherwise -- Failure
930 = zonkTcType ty `thenM` \ ty1 ->
931 failWithTc (ptext SLIT("Type expected but") <+> quotes (ppr ty1) <+> ptext SLIT("found"))
935 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
936 -- Like unifyFunTy, but does not fail; instead just returns Nothing
938 unifyFunKind (TyVarTy tyvar)
939 = getTcTyVar tyvar `thenM` \ maybe_ty ->
941 Just fun_kind -> unifyFunKind fun_kind
942 Nothing -> newKindVar `thenM` \ arg_kind ->
943 newKindVar `thenM` \ res_kind ->
944 putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_`
945 returnM (Just (arg_kind,res_kind))
947 unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
948 unifyFunKind (NoteTy _ ty) = unifyFunKind ty
949 unifyFunKind other = returnM Nothing
952 %************************************************************************
954 \subsection[Unify-context]{Errors and contexts}
956 %************************************************************************
962 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
963 = zonkTcType ty1 `thenM` \ ty1' ->
964 zonkTcType ty2 `thenM` \ ty2' ->
965 returnM (err ty1' ty2')
970 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
971 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
974 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
976 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
977 -- tv1 is zonked already
978 = zonkTcType ty2 `thenM` \ ty2' ->
981 err ty2 = (env2, ptext SLIT("When matching types") <+>
982 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
984 (pp_expected, pp_actual) | swapped = (pp2, pp1)
985 | otherwise = (pp1, pp2)
986 (env1, tv1') = tidyOpenTyVar tidy_env tv1
987 (env2, ty2') = tidyOpenType env1 ty2
991 unifyMisMatch ty1 ty2
992 = zonkTcType ty1 `thenM` \ ty1' ->
993 zonkTcType ty2 `thenM` \ ty2' ->
995 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
996 ppr | isSuperKind (typeKind ty1) = pprKind
997 | otherwise = pprType
998 msg = hang (ptext SLIT("Couldn't match"))
999 4 (sep [quotes (ppr tidy_ty1),
1000 ptext SLIT("against"),
1001 quotes (ppr tidy_ty2)])
1003 failWithTcM (env, msg)
1005 unifyWithSigErr tyvar ty
1006 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1007 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1009 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1010 (env2, tidy_ty) = tidyOpenType env1 ty
1012 unifyCheck problem tyvar ty
1014 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1016 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1017 (env2, tidy_ty) = tidyOpenType env1 ty
1019 msg = case problem of
1020 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1021 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1026 %************************************************************************
1028 \subsection{Checking signature type variables}
1030 %************************************************************************
1032 @checkSigTyVars@ is used after the type in a type signature has been unified with
1033 the actual type found. It then checks that the type variables of the type signature
1035 (a) Still all type variables
1036 eg matching signature [a] against inferred type [(p,q)]
1037 [then a will be unified to a non-type variable]
1039 (b) Still all distinct
1040 eg matching signature [(a,b)] against inferred type [(p,p)]
1041 [then a and b will be unified together]
1043 (c) Not mentioned in the environment
1044 eg the signature for f in this:
1050 Here, f is forced to be monorphic by the free occurence of x.
1052 (d) Not (unified with another type variable that is) in scope.
1053 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1054 when checking the expression type signature, we find that
1055 even though there is nothing in scope whose type mentions r,
1056 nevertheless the type signature for the expression isn't right.
1058 Another example is in a class or instance declaration:
1060 op :: forall b. a -> b
1062 Here, b gets unified with a
1064 Before doing this, the substitution is applied to the signature type variable.
1066 We used to have the notion of a "DontBind" type variable, which would
1067 only be bound to itself or nothing. Then points (a) and (b) were
1068 self-checking. But it gave rise to bogus consequential error messages.
1071 f = (*) -- Monomorphic
1073 g :: Num a => a -> a
1076 Here, we get a complaint when checking the type signature for g,
1077 that g isn't polymorphic enough; but then we get another one when
1078 dealing with the (Num x) context arising from f's definition;
1079 we try to unify x with Int (to default it), but find that x has already
1080 been unified with the DontBind variable "a" from g's signature.
1081 This is really a problem with side-effecting unification; we'd like to
1082 undo g's effects when its type signature fails, but unification is done
1083 by side effect, so we can't (easily).
1085 So we revert to ordinary type variables for signatures, and try to
1086 give a helpful message in checkSigTyVars.
1089 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1090 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1092 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1093 checkSigTyVarsWrt extra_tvs sig_tvs
1094 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1095 check_sig_tyvars extra_tvs' sig_tvs
1098 :: TcTyVarSet -- Global type variables. The universally quantified
1099 -- tyvars should not mention any of these
1100 -- Guaranteed already zonked.
1101 -> [TcTyVar] -- Universally-quantified type variables in the signature
1102 -- Not guaranteed zonked.
1103 -> TcM [TcTyVar] -- Zonked signature type variables
1105 check_sig_tyvars extra_tvs []
1107 check_sig_tyvars extra_tvs sig_tvs
1108 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1109 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1111 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1113 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1114 text "gbl_tvs" <+> ppr gbl_tvs,
1115 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1117 checkM (allDistinctTyVars sig_tys env_tvs)
1118 (complain sig_tys env_tvs) `thenM_`
1120 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1123 complain sig_tys globals
1124 = -- "check" checks each sig tyvar in turn
1126 (env2, emptyVarEnv, [])
1127 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1129 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1131 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1132 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1134 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1136 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1137 -- sig_tyvar is from the signature;
1138 -- ty is what you get if you zonk sig_tyvar and then tidy it
1140 -- acc maps a zonked type variable back to a signature type variable
1141 = case tcGetTyVar_maybe ty of {
1142 Nothing -> -- Error (a)!
1143 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1147 case lookupVarEnv acc tv of {
1148 Just sig_tyvar' -> -- Error (b)!
1149 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1151 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1155 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1156 -- The least comprehensible, so put it last
1158 -- get the local TcIds and TyVars from the environment,
1159 -- and pass them to find_globals (they might have tv free)
1160 then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1161 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1164 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1170 -----------------------
1171 escape_msg sig_tv tv globs
1172 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1173 if notNull globs then
1174 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1175 nest 2 (vcat globs)]
1177 empty -- Sigh. It's really hard to give a good error message
1178 -- all the time. One bad case is an existential pattern match.
1179 -- We rely on the "When..." context to help.
1181 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1182 | otherwise = ptext SLIT("It")
1185 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1186 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1189 These two context are used with checkSigTyVars
1192 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1193 -> TidyEnv -> TcM (TidyEnv, Message)
1194 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1195 = zonkTcType sig_tau `thenM` \ actual_tau ->
1197 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1198 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1199 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1200 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1201 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1203 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),