2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubPat, tcSubExp, tcSub, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTheta,
14 unifyKind, unifyKinds, unifyFunKind,
17 --------------------------------
19 Expected(..), tcInfer, readExpectedType,
20 zapExpectedType, zapExpectedTo, zapExpectedBranches,
21 subFunTys, unifyFunTys,
22 zapToListTy, unifyListTy,
23 zapToTyConApp, unifyTyConApp,
27 #include "HsVersions.h"
29 import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats )
30 import TcHsSyn ( mkHsLet, mkHsDictLam,
31 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
32 import TypeRep ( Type(..), PredType(..), TyNote(..) )
34 import TcRnMonad -- TcType, amongst others
35 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
36 TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),
37 SkolemInfo( GenSkol ), MetaDetails(..),
38 pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
39 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
40 tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
41 typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
42 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
43 pprType, tidySkolemTyVar, isSkolemTyVar )
44 import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
45 openTypeKind, liftedTypeKind, mkArrowKind,
46 isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
47 isSubKind, pprKind, splitKindFunTys )
48 import Inst ( newDicts, instToId, tcInstCall )
49 import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
50 tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
51 newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV,
52 readKindVar, writeKindVar )
53 import TcSimplify ( tcSimplifyCheck )
54 import TcIface ( checkWiredInTyCon )
55 import TcEnv ( tcGetGlobalTyVars, findGlobals )
56 import TyCon ( TyCon, tyConArity, tyConTyVars )
57 import TysWiredIn ( listTyCon )
58 import Id ( Id, mkSysLocal )
59 import Var ( Var, varName, tyVarKind )
60 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
62 import Name ( isSystemName, mkSysTvName )
63 import ErrUtils ( Message )
64 import SrcLoc ( noLoc )
65 import BasicTypes ( Arity )
66 import Util ( notNull, equalLength )
72 * A hole is always filled in with an ordinary type, not another hole.
74 %************************************************************************
76 \subsection{'hole' type variables}
78 %************************************************************************
81 newHole = newMutVar (error "Empty hole in typechecker")
83 tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
85 = do { hole <- newHole
86 ; res <- tc_infer (Infer hole)
87 ; res_ty <- readMutVar hole
88 ; return (res, res_ty) }
90 readExpectedType :: Expected ty -> TcM ty
91 readExpectedType (Infer hole) = readMutVar hole
92 readExpectedType (Check ty) = returnM ty
94 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
95 -- In the inference case, ensure we have a monotype
96 -- (including an unboxed tuple)
97 zapExpectedType (Infer hole) kind
98 = do { ty <- newTyFlexiVarTy kind ;
102 zapExpectedType (Check ty) kind
103 | typeKind ty `isSubKind` kind = return ty
104 | otherwise = do { ty1 <- newTyFlexiVarTy kind
107 -- The unify is to ensure that 'ty' has the desired kind
108 -- For example, in (case e of r -> b) we push an OpenTypeKind
111 zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
112 -- If there is more than one branch in a case expression,
113 -- and exp_ty is a 'hole', all branches must be types, not type schemes,
114 -- otherwise the order in which we check them would affect the result.
115 zapExpectedBranches (MatchGroup [match] _) exp_ty
116 = return exp_ty -- One branch
117 zapExpectedBranches matches (Check ty)
119 zapExpectedBranches matches (Infer hole)
120 = do { -- Many branches, and inference mode,
121 -- so switch to checking mode with a monotype
122 ty <- newTyFlexiVarTy openTypeKind
123 ; writeMutVar hole ty
124 ; return (Check ty) }
126 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
127 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
128 zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
129 -- See Note [Zonk return type]
131 instance Outputable ty => Outputable (Expected ty) where
132 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
133 ppr (Infer hole) = ptext SLIT("Inferring type")
137 %************************************************************************
139 \subsection[Unify-fun]{@unifyFunTy@}
141 %************************************************************************
143 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
144 creation of type variables.
146 * subFunTy is used when we might be faced with a "hole" type variable,
147 in which case we should create two new holes.
149 * unifyFunTy is used when we expect to encounter only "ordinary"
150 type variables, so we should create new ordinary type variables
153 subFunTys :: MatchGroup name
154 -> Expected TcRhoType -- Fail if ty isn't a function type
155 -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
158 subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
159 = -- This is the interesting case
160 ASSERT( null null_matches )
161 do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
162 ; res_hole <- newHole
165 ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
167 -- Extract the answers
168 ; arg_tys <- mapM readMutVar pat_holes
169 ; res_ty <- readMutVar res_hole
171 -- Write the answer into the incoming hole
172 ; writeMutVar hole (mkFunTys arg_tys res_ty)
174 -- And return the answer
177 subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside
178 = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches )
179 -- Assertion just checks that all the matches have the same number of pats
180 do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty
181 ; thing_inside (map Check pat_tys) (Check res_ty) }
183 unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
184 -- Fail if ty isn't a function type, otherwise return arg and result types
185 -- The result types are guaranteed wobbly if the argument is wobbly
187 -- Does not allocate unnecessary meta variables: if the input already is
188 -- a function, we just take it apart. Not only is this efficient, it's important
189 -- for (a) higher rank: the argument might be of form
190 -- (forall a. ty) -> other
191 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
192 -- blow up with the meta var meets the forall
194 -- (b) GADTs: if the argument is not wobbly we do not want the result to be
196 unifyFunTys arity ty = unify_fun_ty True arity ty
198 unify_fun_ty use_refinement arity ty
200 = do { res_ty <- wobblify use_refinement ty
203 unify_fun_ty use_refinement arity (NoteTy _ ty)
204 = unify_fun_ty use_refinement arity ty
206 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
207 = do { details <- condLookupTcTyVar use_refinement tv
209 IndirectTv use' ty' -> unify_fun_ty use' arity ty'
210 other -> unify_fun_help arity ty
213 unify_fun_ty use_refinement arity ty
214 = case tcSplitFunTy_maybe ty of
215 Just (arg,res) -> do { arg' <- wobblify use_refinement arg
216 ; (args', res') <- unify_fun_ty use_refinement (arity-1) res
217 ; return (arg':args', res') }
219 Nothing -> unify_fun_help arity ty
220 -- Usually an error, but ty could be (a Int Bool), which can match
222 unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
223 unify_fun_help arity ty
224 = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
225 ; res <- newTyFlexiVarTy openTypeKind
226 ; unifyTauTy ty (mkFunTys args res)
227 ; return (args, res) }
231 ----------------------
232 zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
233 -> Expected TcSigmaType -- Expected type (T a b c)
234 -> TcM [TcType] -- Element types, a b c
235 -- Insists that the Expected type is not a forall-type
236 -- It's used for wired-in tycons, so we call checkWiredInTyCOn
237 zapToTyConApp tc (Check ty)
238 = do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type
240 zapToTyConApp tc (Infer hole)
241 = do { (tc_app, elt_tys) <- newTyConApp tc
242 ; writeMutVar hole tc_app
243 ; traceTc (text "zap" <+> ppr tc)
244 ; checkWiredInTyCon tc
247 zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists
248 zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
251 ----------------------
252 unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
253 unifyTyConApp tc ty = unify_tc_app True tc ty
254 -- Add a boolean flag to remember whether to use
255 -- the type refinement or not
257 unifyListTy :: TcType -> TcM TcType -- Special case for lists
258 unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
262 unify_tc_app use_refinement tc (NoteTy _ ty)
263 = unify_tc_app use_refinement tc ty
265 unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
266 = do { details <- condLookupTcTyVar use_refinement tyvar
268 IndirectTv use' ty' -> unify_tc_app use' tc ty'
269 other -> unify_tc_app_help tc ty
272 unify_tc_app use_refinement tc ty
273 | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
275 = ASSERT( tyConArity tycon == length arg_tys ) -- ty::*
276 mapM (wobblify use_refinement) arg_tys
278 unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
280 unify_tc_app_help tc ty -- Revert to ordinary unification
281 = do { (tc_app, arg_tys) <- newTyConApp tc
282 ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
283 unifyMisMatch ty tc_app
285 { unifyTauTy ty tc_app
286 ; returnM arg_tys } }
289 ----------------------
290 unifyAppTy :: TcType -- Type to split: m a
291 -> TcM (TcType, TcType) -- (m,a)
294 unifyAppTy ty = unify_app_ty True ty
296 unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty
298 unify_app_ty use ty@(TyVarTy tyvar)
299 = do { details <- condLookupTcTyVar use tyvar
301 IndirectTv use' ty' -> unify_app_ty use' ty'
302 other -> unify_app_ty_help ty
306 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
307 = do { fun' <- wobblify use fun_ty
308 ; arg' <- wobblify use arg_ty
309 ; return (fun', arg') }
311 | otherwise = unify_app_ty_help ty
313 unify_app_ty_help ty -- Revert to ordinary unification
314 = do { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind)
315 ; arg_ty <- newTyFlexiVarTy liftedTypeKind
316 ; unifyTauTy (mkAppTy fun_ty arg_ty) ty
317 ; return (fun_ty, arg_ty) }
320 ----------------------
321 wobblify :: Bool -- True <=> don't wobblify
324 -- Return a wobbly type. At the moment we do that by
325 -- allocating a fresh meta type variable.
326 wobblify True ty = return ty
327 wobblify False ty = do { uniq <- newUnique
328 ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
331 ; return (mkTyVarTy tv) }
333 ----------------------
334 newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
335 newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
336 ; return (mkTyConApp tc args, args) }
340 %************************************************************************
342 \subsection{Subsumption}
344 %************************************************************************
346 All the tcSub calls have the form
348 tcSub expected_ty offered_ty
350 offered_ty <= expected_ty
352 That is, that a value of type offered_ty is acceptable in
353 a place expecting a value of type expected_ty.
355 It returns a coercion function
356 co_fn :: offered_ty -> expected_ty
357 which takes an HsExpr of type offered_ty into one of type
361 -----------------------
362 -- tcSubExp is used for expressions
363 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
365 tcSubExp (Infer hole) offered_ty
366 = do { offered' <- zonkTcType offered_ty
367 -- Note [Zonk return type]
368 -- zonk to take advantage of the current GADT type refinement.
369 -- If we don't we get spurious "existential type variable escapes":
370 -- case (x::Maybe a) of
371 -- Just b (y::b) -> y
372 -- We need the refinement [b->a] to be applied to the result type
373 ; writeMutVar hole offered'
374 ; return idCoercion }
376 tcSubExp (Check expected_ty) offered_ty
377 = tcSub expected_ty offered_ty
379 -----------------------
380 -- tcSubPat is used for patterns
381 tcSubPat :: TcSigmaType -- Pattern type signature
382 -> Expected TcSigmaType -- Type from context
384 -- In patterns we insist on an exact match; hence no CoFn returned
385 -- See Note [Pattern coercions] in TcPat
386 -- However, we can't call unify directly, because both types might be
387 -- polymorphic; hence the call to tcSub, followed by a check for
388 -- the identity coercion
390 tcSubPat sig_ty (Infer hole)
391 = do { sig_ty' <- zonkTcType sig_ty
392 ; writeMutVar hole sig_ty' -- See notes with tcSubExp above
395 tcSubPat sig_ty (Check exp_ty)
396 = do { co_fn <- tcSub sig_ty exp_ty
398 ; if isIdCoercion co_fn then
401 unifyMisMatch sig_ty exp_ty }
406 %************************************************************************
408 tcSub: main subsumption-check code
410 %************************************************************************
412 No holes expected now. Add some error-check context info.
416 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
417 -- tcSub exp act checks that
419 tcSub expected_ty actual_ty
420 = traceTc (text "tcSub" <+> details) `thenM_`
421 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
422 (tc_sub expected_ty expected_ty actual_ty actual_ty)
424 details = vcat [text "Expected:" <+> ppr expected_ty,
425 text "Actual: " <+> ppr actual_ty]
428 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
429 -> TcSigmaType -- ..and after
430 -> TcSigmaType -- actual_ty, before
431 -> TcSigmaType -- ..and after
434 -----------------------------------
436 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
437 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
439 -----------------------------------
440 -- Generalisation case
441 -- actual_ty: d:Eq b => b->b
442 -- expected_ty: forall a. Ord a => a->a
443 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
445 -- It is essential to do this *before* the specialisation case
446 -- Example: f :: (Eq a => a->a) -> ...
447 -- g :: Ord b => b->b
450 tc_sub exp_sty expected_ty act_sty actual_ty
451 | isSigmaTy expected_ty
452 = tcGen expected_ty (tyVarsOfType actual_ty) (
453 -- It's really important to check for escape wrt the free vars of
454 -- both expected_ty *and* actual_ty
455 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
456 ) `thenM` \ (gen_fn, co_fn) ->
457 returnM (gen_fn <.> co_fn)
459 -----------------------------------
460 -- Specialisation case:
461 -- actual_ty: forall a. Ord a => a->a
462 -- expected_ty: Int -> Int
463 -- co_fn e = e Int dOrdInt
465 tc_sub exp_sty expected_ty act_sty actual_ty
466 | isSigmaTy actual_ty
467 = tcInstCall InstSigOrigin actual_ty `thenM` \ (inst_fn, _, body_ty) ->
468 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
469 returnM (co_fn <.> inst_fn)
471 -----------------------------------
474 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
475 = tcSub_fun exp_arg exp_res act_arg act_res
477 -----------------------------------
478 -- Type variable meets function: imitate
480 -- NB 1: we can't just unify the type variable with the type
481 -- because the type might not be a tau-type, and we aren't
482 -- allowed to instantiate an ordinary type variable with
485 -- NB 2: can we short-cut to an error case?
486 -- when the arg/res is not a tau-type?
487 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
489 -- is perfectly fine, because we can instantiate f's type to a monotype
491 -- However, we get can get jolly unhelpful error messages.
492 -- e.g. foo = id runST
494 -- Inferred type is less polymorphic than expected
495 -- Quantified type variable `s' escapes
496 -- Expected type: ST s a -> t
497 -- Inferred type: (forall s1. ST s1 a) -> a
498 -- In the first argument of `id', namely `runST'
499 -- In a right-hand side of function `foo': id runST
501 -- I'm not quite sure what to do about this!
503 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
504 = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty
505 ; tcSub_fun exp_arg exp_res act_arg act_res }
507 tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
508 = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
509 ; tcSub_fun exp_arg exp_res act_arg act_res }
511 -----------------------------------
513 -- If none of the above match, we revert to the plain unifier
514 tc_sub exp_sty expected_ty act_sty actual_ty
515 = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
520 tcSub_fun exp_arg exp_res act_arg act_res
521 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
522 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
523 newUnique `thenM` \ uniq ->
525 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
526 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
527 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
528 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
529 coercion | isIdCoercion co_fn_arg,
530 isIdCoercion co_fn_res = idCoercion
531 | otherwise = mkCoercion co_fn
533 co_fn e = DictLam [arg_id]
534 (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
535 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
536 -- HsVar arg_id :: HsExpr exp_arg
537 -- co_fn_arg $it :: HsExpr act_arg
538 -- HsApp e $it :: HsExpr act_res
539 -- co_fn_res $it :: HsExpr exp_res
545 %************************************************************************
547 \subsection{Generalisation}
549 %************************************************************************
552 tcGen :: TcSigmaType -- expected_ty
553 -> TcTyVarSet -- Extra tyvars that the universally
554 -- quantified tyvars of expected_ty
555 -- must not be unified
556 -> (TcRhoType -> TcM result) -- spec_ty
557 -> TcM (ExprCoFn, result)
558 -- The expression has type: spec_ty -> expected_ty
560 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
561 -- If not, the call is a no-op
562 = do { -- We want the GenSkol info in the skolemised type variables to
563 -- mention the *instantiated* tyvar names, so that we get a
564 -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
565 -- Hence the tiresome but innocuous fixM
566 ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
567 do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
568 ; span <- getSrcSpanM
569 ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
570 ; return ((forall_tvs, theta, rho_ty), skol_info) })
573 ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
574 text "expected_ty" <+> ppr expected_ty,
575 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
576 text "free_tvs" <+> ppr free_tvs,
577 text "forall_tvs" <+> ppr forall_tvs])
580 -- Type-check the arg and unify with poly type
581 ; (result, lie) <- getLIE (thing_inside rho_ty)
583 -- Check that the "forall_tvs" havn't been constrained
584 -- The interesting bit here is that we must include the free variables
585 -- of the expected_ty. Here's an example:
586 -- runST (newVar True)
587 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
588 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
589 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
590 -- So now s' isn't unconstrained because it's linked to a.
591 -- Conclusion: include the free vars of the expected_ty in the
592 -- list of "free vars" for the signature check.
594 ; dicts <- newDicts (SigOrigin skol_info) theta
595 ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
597 ; checkSigTyVarsWrt free_tvs forall_tvs
598 ; traceTc (text "tcGen:done")
601 -- This HsLet binds any Insts which came out of the simplification.
602 -- It's a bit out of place here, but using AbsBind involves inventing
603 -- a couple of new names which seems worse.
604 dict_ids = map instToId dicts
605 co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
606 ; returnM (mkCoercion co_fn, result) }
608 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
609 sig_msg = ptext SLIT("expected type of an expression")
614 %************************************************************************
616 \subsection[Unify-exported]{Exported unification functions}
618 %************************************************************************
620 The exported functions are all defined as versions of some
621 non-exported generic functions.
623 Unify two @TauType@s. Dead straightforward.
626 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
627 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
628 = -- The unifier should only ever see tau-types
629 -- (no quantification whatsoever)
630 ASSERT2( isTauTy ty1, ppr ty1 )
631 ASSERT2( isTauTy ty2, ppr ty2 )
632 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
633 uTys True ty1 ty1 True ty2 ty2
635 unifyTheta :: TcThetaType -> TcThetaType -> TcM ()
636 unifyTheta theta1 theta2
637 = do { checkTc (equalLength theta1 theta2)
638 (ptext SLIT("Contexts differ in length"))
639 ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) }
642 @unifyTauTyList@ unifies corresponding elements of two lists of
643 @TauType@s. It uses @uTys@ to do the real work. The lists should be
644 of equal length. We charge down the list explicitly so that we can
645 complain if their lengths differ.
648 unifyTauTyLists :: Bool -> -- Allow refinements on tys1
650 Bool -> -- Allow refinements on tys2
651 [TcTauType] -> TcM ()
652 -- Precondition: lists must be same length
653 -- Having the caller check gives better error messages
654 -- Actually the caller neve does need to check; see Note [Tycon app]
655 unifyTauTyLists r1 [] r2 [] = returnM ()
656 unifyTauTyLists r1 (ty1:tys1) r2 (ty2:tys2) = uTys r1 ty1 ty1 r2 ty2 ty2 `thenM_`
657 unifyTauTyLists r1 tys1 r2 tys2
658 unifyTauTyLists r1 ty1s r2 ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
661 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
662 all together. It is used, for example, when typechecking explicit
663 lists, when all the elts should be of the same type.
666 unifyTauTyList :: [TcTauType] -> TcM ()
667 unifyTauTyList [] = returnM ()
668 unifyTauTyList [ty] = returnM ()
669 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
673 %************************************************************************
675 \subsection[Unify-uTys]{@uTys@: getting down to business}
677 %************************************************************************
679 @uTys@ is the heart of the unifier. Each arg happens twice, because
680 we want to report errors in terms of synomyms if poss. The first of
681 the pair is used in error messages only; it is always the same as the
682 second, except that if the first is a synonym then the second may be a
683 de-synonym'd version. This way we get better error messages.
685 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
688 uTys :: Bool -- Allow refinements to ty1
689 -> TcTauType -> TcTauType -- Error reporting ty1 and real ty1
690 -- ty1 is the *expected* type
691 -> Bool -- Allow refinements to ty2
692 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
693 -- ty2 is the *actual* type
696 -- Always expand synonyms (see notes at end)
697 -- (this also throws away FTVs)
698 uTys r1 ps_ty1 (NoteTy n1 ty1) r2 ps_ty2 ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
699 uTys r1 ps_ty1 ty1 r2 ps_ty2 (NoteTy n2 ty2) = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
701 -- Variables; go for uVar
702 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
703 uTys r1 ps_ty1 ty1 r2 ps_ty2 (TyVarTy tyvar2) = uVar True r2 tyvar2 r1 ps_ty1 ty1
704 -- "True" means args swapped
707 uTys r1 _ (PredTy (IParam n1 t1)) r2 _ (PredTy (IParam n2 t2))
708 | n1 == n2 = uTys r1 t1 t1 r2 t2 t2
709 uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2))
710 | c1 == c2 = unifyTauTyLists r1 tys1 r2 tys2
711 -- Guaranteed equal lengths because the kinds check
713 -- Functions; just check the two parts
714 uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2)
715 = uTys r1 fun1 fun1 r2 fun2 fun2 `thenM_` uTys r1 arg1 arg1 r2 arg2 arg2
717 -- Type constructors must match
718 uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2)
719 | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2
720 -- See Note [TyCon app]
722 -- Applications need a bit of care!
723 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
724 -- NB: we've already dealt with type variables and Notes,
725 -- so if one type is an App the other one jolly well better be too
726 uTys r1 ps_ty1 (AppTy s1 t1) r2 ps_ty2 ty2
727 = case tcSplitAppTy_maybe ty2 of
728 Just (s2,t2) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
729 Nothing -> unifyMisMatch ps_ty1 ps_ty2
731 -- Now the same, but the other way round
732 -- Don't swap the types, because the error messages get worse
733 uTys r1 ps_ty1 ty1 r2 ps_ty2 (AppTy s2 t2)
734 = case tcSplitAppTy_maybe ty1 of
735 Just (s1,t1) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
736 Nothing -> unifyMisMatch ps_ty1 ps_ty2
738 -- Not expecting for-alls in unification
739 -- ... but the error message from the unifyMisMatch more informative
740 -- than a panic message!
742 -- Anything else fails
743 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
748 When we find two TyConApps, the argument lists are guaranteed equal
749 length. Reason: intially the kinds of the two types to be unified is
750 the same. The only way it can become not the same is when unifying two
751 AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
752 the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
753 which we do, that ensures that f1,f2 have the same kind; and that
754 means a1,a2 have the same kind. And now the argument repeats.
759 If you are tempted to make a short cut on synonyms, as in this
763 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
764 -- NO = if (con1 == con2) then
765 -- NO -- Good news! Same synonym constructors, so we can shortcut
766 -- NO -- by unifying their arguments and ignoring their expansions.
767 -- NO unifyTauTypeLists args1 args2
769 -- NO -- Never mind. Just expand them and try again
773 then THINK AGAIN. Here is the whole story, as detected and reported
774 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
776 Here's a test program that should detect the problem:
780 x = (1 :: Bogus Char) :: Bogus Bool
783 The problem with [the attempted shortcut code] is that
787 is not a sufficient condition to be able to use the shortcut!
788 You also need to know that the type synonym actually USES all
789 its arguments. For example, consider the following type synonym
790 which does not use all its arguments.
795 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
796 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
797 would fail, even though the expanded forms (both \tr{Int}) should
800 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
801 unnecessarily bind \tr{t} to \tr{Char}.
803 ... You could explicitly test for the problem synonyms and mark them
804 somehow as needing expansion, perhaps also issuing a warning to the
809 %************************************************************************
811 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
813 %************************************************************************
815 @uVar@ is called when at least one of the types being unified is a
816 variable. It does {\em not} assume that the variable is a fixed point
817 of the substitution; rather, notice that @uVar@ (defined below) nips
818 back into @uTys@ if it turns out that the variable is already bound.
821 uVar :: Bool -- False => tyvar is the "expected"
822 -- True => ty is the "expected" thing
823 -> Bool -- True, allow refinements to tv1, False don't
825 -> Bool -- Allow refinements to ty2?
826 -> TcTauType -> TcTauType -- printing and real versions
829 uVar swapped r1 tv1 r2 ps_ty2 ty2
830 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
831 condLookupTcTyVar r1 tv1 `thenM` \ details ->
833 IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
834 | otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
835 DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
838 uDoneVar :: Bool -- Args are swapped
839 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
840 -> Bool -- Allow refinements to ty2
841 -> TcTauType -> TcTauType -- Type 2
843 -- Invariant: tyvar 1 is not unified with anything
845 uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
846 = -- Expand synonyms; ignore FTVs
847 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
849 uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)
850 -- Same type variable => no-op
854 -- Distinct type variables
856 = do { lookup2 <- condLookupTcTyVar r2 tv2
858 IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2'
859 DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2
862 uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable
864 MetaTv ref1 -> do { -- Do the occurs check, and check that we are not
865 -- unifying a type variable with a polytype
866 -- Returns a zonked type ready for the update
867 ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
868 ; updateMeta swapped tv1 ref1 ty2 }
870 skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
874 uDoneVars :: Bool -- Args are swapped
875 -> TcTyVar -> TcTyVarDetails -- Tyvar 1
876 -> TcTyVar -> TcTyVarDetails -- Tyvar 2
878 -- Invarant: the type variables are distinct,
879 -- and are not already unified with anything
881 uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
883 MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
884 other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
885 -- Note that updateMeta does a sub-kind check
886 -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
890 update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
891 -- Update the variable with least kind info
892 -- See notes on type inference in Kind.lhs
893 -- The "nicer to" part only applies if the two kinds are the same,
894 -- so we can choose which to do.
896 nicer_to_update_tv2 = isSystemName (varName tv2)
897 -- Try to update sys-y type variables in preference to ones
898 -- gotten (say) by instantiating a polymorphic function with
899 -- a user-written type sig
901 uDoneVars swapped tv1 (SkolemTv _) tv2 details2
903 MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
904 other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
906 uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
908 MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
909 SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
910 other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)
913 updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
914 -- Update tv1, which is flexi; occurs check is alrady done
915 updateMeta swapped tv1 ref1 ty2
916 = do { checkKinds swapped tv1 ty2
917 ; writeMutVar ref1 (Indirect ty2) }
921 checkKinds swapped tv1 ty2
922 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
923 -- ty2 has been zonked at this stage, which ensures that
924 -- its kind has as much boxity information visible as possible.
925 | tk2 `isSubKind` tk1 = returnM ()
928 -- Either the kinds aren't compatible
929 -- (can happen if we unify (a b) with (c d))
930 -- or we are unifying a lifted type variable with an
931 -- unlifted type: e.g. (id 3#) is illegal
932 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
933 unifyKindMisMatch k1 k2
935 (k1,k2) | swapped = (tk2,tk1)
936 | otherwise = (tk1,tk2)
942 checkValue tv1 r2 ps_ty2 non_var_ty2
943 -- Do the occurs check, and check that we are not
944 -- unifying a type variable with a polytype
945 -- Return the type to update the type variable with, or fail
947 -- Basically we want to update tv1 := ps_ty2
948 -- because ps_ty2 has type-synonym info, which improves later error messages
953 -- f :: (A a -> a -> ()) -> ()
957 -- x = f (\ x p -> p x)
959 -- In the application (p x), we try to match "t" with "A t". If we go
960 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
961 -- an infinite loop later.
962 -- But we should not reject the program, because A t = ().
963 -- Rather, we should bind t to () (= non_var_ty2).
965 -- That's why we have this two-state occurs-check
966 = zonk_tc_type r2 ps_ty2 `thenM` \ ps_ty2' ->
967 case okToUnifyWith tv1 ps_ty2' of {
968 Nothing -> returnM ps_ty2' ; -- Success
971 zonk_tc_type r2 non_var_ty2 `thenM` \ non_var_ty2' ->
972 case okToUnifyWith tv1 non_var_ty2' of
973 Nothing -> -- This branch rarely succeeds, except in strange cases
974 -- like that in the example above
977 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
980 zonk_tc_type refine ty
981 = zonkType (\tv -> return (TyVarTy tv)) refine ty
982 -- We may already be inside a wobbly type t2, and
983 -- should take that into account here
985 data Problem = OccurCheck | NotMonoType
987 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
988 -- (okToUnifyWith tv ty) checks whether it's ok to unify
991 -- Just p => not ok, problem p
996 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
997 | otherwise = Nothing
998 ok (AppTy t1 t2) = ok t1 `and` ok t2
999 ok (FunTy t1 t2) = ok t1 `and` ok t2
1000 ok (TyConApp _ ts) = oks ts
1001 ok (ForAllTy _ _) = Just NotMonoType
1002 ok (PredTy st) = ok_st st
1003 ok (NoteTy (FTVNote _) t) = ok t
1004 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
1005 -- Type variables may be free in t1 but not t2
1006 -- A forall may be in t2 but not t1
1008 oks ts = foldr (and . ok) Nothing ts
1010 ok_st (ClassP _ ts) = oks ts
1011 ok_st (IParam _ t) = ok t
1014 Just p `and` m = Just p
1018 %************************************************************************
1022 %************************************************************************
1024 Unifying kinds is much, much simpler than unifying types.
1027 unifyKind :: TcKind -- Expected
1030 unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
1031 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
1033 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
1034 unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
1035 -- Respect sub-kinding
1037 unifyKind (FunKind a1 r1) (FunKind a2 r2)
1038 = do { unifyKind a2 a1; unifyKind r1 r2 }
1039 -- Notice the flip in the argument,
1040 -- so that the sub-kinding works right
1042 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
1043 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
1044 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1046 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1047 unifyKinds [] [] = returnM ()
1048 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
1050 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1053 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1054 uKVar swapped kv1 k2
1055 = do { mb_k1 <- readKindVar kv1
1057 Nothing -> uUnboundKVar swapped kv1 k2
1058 Just k1 | swapped -> unifyKind k2 k1
1059 | otherwise -> unifyKind k1 k2 }
1062 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1063 uUnboundKVar swapped kv1 k2@(KindVar kv2)
1064 | kv1 == kv2 = returnM ()
1065 | otherwise -- Distinct kind variables
1066 = do { mb_k2 <- readKindVar kv2
1068 Just k2 -> uUnboundKVar swapped kv1 k2
1069 Nothing -> writeKindVar kv1 k2 }
1071 uUnboundKVar swapped kv1 non_var_k2
1072 = do { k2' <- zonkTcKind non_var_k2
1073 ; kindOccurCheck kv1 k2'
1074 ; k2'' <- kindSimpleKind swapped k2'
1075 -- KindVars must be bound only to simple kinds
1076 -- Polarities: (kindSimpleKind True ?) succeeds
1077 -- returning *, corresponding to unifying
1080 ; writeKindVar kv1 k2'' }
1083 kindOccurCheck kv1 k2 -- k2 is zonked
1084 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1086 not_in (KindVar kv2) = kv1 /= kv2
1087 not_in (FunKind a2 r2) = not_in a2 && not_in r2
1090 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1091 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1092 -- If the flag is False, it requires k <: sk
1093 -- E.g. kindSimpleKind False ?? = *
1094 -- What about (kv -> *) :=: ?? -> *
1095 kindSimpleKind orig_swapped orig_kind
1096 = go orig_swapped orig_kind
1098 go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
1100 ; return (FunKind k1' k2') }
1101 go True OpenTypeKind = return liftedTypeKind
1102 go True ArgTypeKind = return liftedTypeKind
1103 go sw LiftedTypeKind = return liftedTypeKind
1104 go sw k@(KindVar _) = return k -- KindVars are always simple
1105 go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1106 <+> ppr orig_swapped <+> ppr orig_kind)
1107 -- I think this can't actually happen
1109 -- T v = MkT v v must be a type
1110 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1113 kindOccurCheckErr tyvar ty
1114 = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1115 2 (sep [ppr tyvar, char '=', ppr ty])
1117 unifyKindMisMatch ty1 ty2
1118 = zonkTcKind ty1 `thenM` \ ty1' ->
1119 zonkTcKind ty2 `thenM` \ ty2' ->
1121 msg = hang (ptext SLIT("Couldn't match kind"))
1122 2 (sep [quotes (ppr ty1'),
1123 ptext SLIT("against"),
1130 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1131 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1133 unifyFunKind (KindVar kvar)
1134 = readKindVar kvar `thenM` \ maybe_kind ->
1136 Just fun_kind -> unifyFunKind fun_kind
1137 Nothing -> do { arg_kind <- newKindVar
1138 ; res_kind <- newKindVar
1139 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1140 ; returnM (Just (arg_kind,res_kind)) }
1142 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1143 unifyFunKind other = returnM Nothing
1146 %************************************************************************
1148 \subsection[Unify-context]{Errors and contexts}
1150 %************************************************************************
1156 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1157 = zonkTcType ty1 `thenM` \ ty1' ->
1158 zonkTcType ty2 `thenM` \ ty2' ->
1159 returnM (err ty1' ty2')
1161 err ty1 ty2 = (env1,
1164 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1165 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1168 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1170 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1171 -- tv1 and ty2 are zonked already
1174 msg = (env2, ptext SLIT("When matching the kinds of") <+>
1175 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1177 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1178 | otherwise = (pp1, pp2)
1179 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1180 (env2, ty2') = tidyOpenType env1 ty2
1181 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1182 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1184 unifyMisMatch ty1 ty2
1185 = do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
1186 ; (env2, pp2, extra2) <- ppr_ty env1 ty2
1187 ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)],
1188 nest 2 extra1, nest 2 extra2]
1190 failWithTcM (env2, msg) }
1192 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1194 = do { ty' <- zonkTcType ty
1195 ; let (env1,tidy_ty) = tidyOpenType env ty'
1196 simple_result = (env1, quotes (ppr tidy_ty), empty)
1199 | isSkolemTyVar tv -> return (env2, pp_rigid tv',
1201 | otherwise -> return simple_result
1203 (env2, tv') = tidySkolemTyVar env1 tv
1204 other -> return simple_result }
1206 pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
1208 unifyCheck problem tyvar ty
1210 2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1212 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1213 (env2, tidy_ty) = tidyOpenType env1 ty
1215 msg = case problem of
1216 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1217 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1221 %************************************************************************
1225 %************************************************************************
1227 ---------------------------
1228 -- We would like to get a decent error message from
1229 -- (a) Under-applied type constructors
1230 -- f :: (Maybe, Maybe)
1231 -- (b) Over-applied type constructors
1232 -- f :: Int x -> Int x
1236 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1237 -- A fancy wrapper for 'unifyKind', which tries
1238 -- to give decent error messages.
1239 checkExpectedKind ty act_kind exp_kind
1240 | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1243 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
1245 Just _ -> returnM () ; -- Unification succeeded
1248 -- So there's definitely an error
1249 -- Now to find out what sort
1250 zonkTcKind exp_kind `thenM` \ exp_kind ->
1251 zonkTcKind act_kind `thenM` \ act_kind ->
1253 let (exp_as, _) = splitKindFunTys exp_kind
1254 (act_as, _) = splitKindFunTys act_kind
1255 n_exp_as = length exp_as
1256 n_act_as = length act_as
1258 err | n_exp_as < n_act_as -- E.g. [Maybe]
1259 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1261 -- Now n_exp_as >= n_act_as. In the next two cases,
1262 -- n_exp_as == 0, and hence so is n_act_as
1263 | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1264 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1265 <+> ptext SLIT("is unlifted")
1267 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1268 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1269 <+> ptext SLIT("is lifted")
1271 | otherwise -- E.g. Monad [Int]
1272 = ptext SLIT("Kind mis-match")
1274 more_info = sep [ ptext SLIT("Expected kind") <+>
1275 quotes (pprKind exp_kind) <> comma,
1276 ptext SLIT("but") <+> quotes (ppr ty) <+>
1277 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
1279 failWithTc (err $$ more_info)
1283 %************************************************************************
1285 \subsection{Checking signature type variables}
1287 %************************************************************************
1289 @checkSigTyVars@ checks that a set of universally quantified type varaibles
1290 are not mentioned in the environment. In particular:
1292 (a) Not mentioned in the type of a variable in the envt
1293 eg the signature for f in this:
1299 Here, f is forced to be monorphic by the free occurence of x.
1301 (d) Not (unified with another type variable that is) in scope.
1302 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1303 when checking the expression type signature, we find that
1304 even though there is nothing in scope whose type mentions r,
1305 nevertheless the type signature for the expression isn't right.
1307 Another example is in a class or instance declaration:
1309 op :: forall b. a -> b
1311 Here, b gets unified with a
1313 Before doing this, the substitution is applied to the signature type variable.
1316 checkSigTyVars :: [TcTyVar] -> TcM ()
1317 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1319 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1320 checkSigTyVarsWrt extra_tvs sig_tvs
1321 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1322 check_sig_tyvars extra_tvs' sig_tvs
1325 :: TcTyVarSet -- Global type variables. The universally quantified
1326 -- tyvars should not mention any of these
1327 -- Guaranteed already zonked.
1328 -> [TcTyVar] -- Universally-quantified type variables in the signature
1329 -- Guaranteed to be skolems
1331 check_sig_tyvars extra_tvs []
1333 check_sig_tyvars extra_tvs sig_tvs
1334 = ASSERT( all isSkolemTyVar sig_tvs )
1335 do { gbl_tvs <- tcGetGlobalTyVars
1336 ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1337 text "gbl_tvs" <+> ppr gbl_tvs,
1338 text "extra_tvs" <+> ppr extra_tvs]))
1340 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1341 ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
1342 (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
1345 bleatEscapedTvs :: TcTyVarSet -- The global tvs
1346 -> [TcTyVar] -- The possibly-escaping type variables
1347 -> [TcTyVar] -- The zonked versions thereof
1349 -- Complain about escaping type variables
1350 -- We pass a list of type variables, at least one of which
1351 -- escapes. The first list contains the original signature type variable,
1352 -- while the second contains the type variable it is unified to (usually itself)
1353 bleatEscapedTvs globals sig_tvs zonked_tvs
1354 = do { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs)
1355 ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) }
1357 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1358 (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs
1360 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1362 check (tidy_env, msgs) (sig_tv, zonked_tv)
1363 | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
1365 = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
1366 ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
1368 -----------------------
1369 escape_msg sig_tv zonked_tv globs
1371 = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")],
1372 nest 2 (vcat globs)]
1374 = msg <+> ptext SLIT("escapes")
1375 -- Sigh. It's really hard to give a good error message
1376 -- all the time. One bad case is an existential pattern match.
1377 -- We rely on the "When..." context to help.
1379 msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to
1381 | sig_tv == zonked_tv = empty
1382 | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which")
1385 These two context are used with checkSigTyVars
1388 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1389 -> TidyEnv -> TcM (TidyEnv, Message)
1390 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1391 = zonkTcType sig_tau `thenM` \ actual_tau ->
1393 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1394 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1395 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1396 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1397 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1399 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),